Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 237598)
+++ sem_prag.adb	(working copy)
@@ -26277,9 +26277,10 @@
    -----------------------------------
 
    function Build_Pragma_Check_Equivalent
-     (Prag     : Node_Id;
-      Subp_Id  : Entity_Id := Empty;
-      Inher_Id : Entity_Id := Empty) return Node_Id
+     (Prag           : Node_Id;
+      Subp_Id        : Entity_Id := Empty;
+      Inher_Id       : Entity_Id := Empty;
+      Keep_Pragma_Id : Boolean := False) return Node_Id
    is
       Map : Elist_Id;
       --  List containing the following mappings
@@ -26361,6 +26362,15 @@
                    & "for&#", N, Current_Scope);
             end if;
 
+            --  Update type of function call node, which should be the same as
+            --  the function's return type.
+
+            if Is_Subprogram (Entity (N))
+              and then Nkind (Parent (N)) = N_Function_Call
+            then
+               Set_Etype (Parent (N), Etype (Entity (N)));
+            end if;
+
          --  The whole expression will be reanalyzed
 
          elsif Nkind (N) in N_Has_Etype then
@@ -26595,7 +26605,6 @@
 
       Set_Analyzed          (Check_Prag, False);
       Set_Comes_From_Source (Check_Prag, False);
-      Set_Class_Present     (Check_Prag, False);
 
       --  The tree of the original pragma may contain references to the
       --  formal parameters of the related subprogram. At the same time
@@ -26621,16 +26630,21 @@
          Nam := Prag_Nam;
       end if;
 
-      --  Convert the copy into pragma Check by correcting the name and adding
-      --  a check_kind argument.
+      --  Unless Keep_Pragma_Id is True in order to keep the identifier of
+      --  the copied pragma in the newly created pragma, convert the copy into
+      --  pragma Check by correcting the name and adding a check_kind argument.
 
-      Set_Pragma_Identifier
-        (Check_Prag, Make_Identifier (Loc, Name_Check));
+      if not Keep_Pragma_Id then
+         Set_Class_Present (Check_Prag, False);
 
-      Prepend_To (Pragma_Argument_Associations (Check_Prag),
-        Make_Pragma_Argument_Association (Loc,
-          Expression => Make_Identifier (Loc, Nam)));
+         Set_Pragma_Identifier
+           (Check_Prag, Make_Identifier (Loc, Name_Check));
 
+         Prepend_To (Pragma_Argument_Associations (Check_Prag),
+           Make_Pragma_Argument_Association (Loc,
+             Expression => Make_Identifier (Loc, Nam)));
+      end if;
+
       --  Update the error message when the pragma is inherited
 
       if Present (Inher_Id) then
@@ -27154,7 +27168,8 @@
                end if;
 
                New_Prag :=
-                 Build_Pragma_Check_Equivalent (Prag, Subp, Parent_Subp);
+                 Build_Pragma_Check_Equivalent (Prag, Subp, Parent_Subp,
+                                                Keep_Pragma_Id => True);
                Insert_After (Unit_Declaration_Node (Subp), New_Prag);
                Preanalyze (New_Prag);
 
Index: sem_prag.ads
===================================================================
--- sem_prag.ads	(revision 237595)
+++ sem_prag.ads	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -245,14 +245,18 @@
    --  Perform preanalysis of pragma Test_Case
 
    function Build_Pragma_Check_Equivalent
-     (Prag     : Node_Id;
-      Subp_Id  : Entity_Id := Empty;
-      Inher_Id : Entity_Id := Empty) return Node_Id;
-   --  Transform a [refined] pre- or postcondition denoted by Prag into an
+     (Prag           : Node_Id;
+      Subp_Id        : Entity_Id := Empty;
+      Inher_Id       : Entity_Id := Empty;
+      Keep_Pragma_Id : Boolean := False) return Node_Id;
+   --  Transform a pre- or [refined] postcondition denoted by Prag into an
    --  equivalent pragma Check. When the pre- or postcondition is inherited,
-   --  the routine replaces the references of all formals of Inher_Id and
-   --  primitive operations of its controlling type by references to the
-   --  corresponding entities of Subp_Id and the descendant type.
+   --  the routine replaces the references of all formals of Inher_Id
+   --  and primitive operations of its controlling type by references
+   --  to the corresponding entities of Subp_Id and the descendant type.
+   --  Keep_Pragma_Id is True when the newly created pragma should be
+   --  in fact of the same kind as the source pragma Prag. This is used
+   --  in GNATprove_Mode to generate the inherited pre- and postconditions.
 
    procedure Check_Applicable_Policy (N : Node_Id);
    --  N is either an N_Aspect or an N_Pragma node. There are two cases. If
Index: sinfo.ads
===================================================================
--- sinfo.ads	(revision 237595)
+++ sinfo.ads	(working copy)
@@ -7618,6 +7618,10 @@
       --  source, or because a Pre (resp. Post) aspect specification has been
       --  broken into AND THEN sections. See Split_PPC for details.
 
+      --  In GNATprove mode, the inherited classwide pre- and postconditions
+      --  (suitably specialized for the specific type of the overriding
+      --  operation) are also in this list.
+
       --  Contract_Test_Cases contains a collection of pragmas that correspond
       --  to aspects/pragmas Contract_Cases and Test_Case. The ordering in the
       --  list is in LIFO fashion.
