Index: exp_spark.adb
===================================================================
--- exp_spark.adb	(revision 235481)
+++ exp_spark.adb	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          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- --
@@ -42,10 +42,6 @@
    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
    --  Perform name evaluation for a renamed object
 
-   procedure Expand_Potential_Renaming (N : Node_Id);
-   --  N denotes a N_Identifier or N_Expanded_Name. If N references a renaming,
-   --  replace N with the renamed object.
-
    ------------------
    -- Expand_SPARK --
    ------------------
@@ -73,7 +69,7 @@
 
          when N_Expanded_Name |
               N_Identifier    =>
-            Expand_Potential_Renaming (N);
+            Expand_SPARK_Potential_Renaming (N);
 
          when N_Object_Renaming_Declaration =>
             Expand_SPARK_N_Object_Renaming_Declaration (N);
@@ -116,41 +112,41 @@
       Evaluate_Name (Name (N));
    end Expand_SPARK_N_Object_Renaming_Declaration;
 
-   -------------------------------
-   -- Expand_Potential_Renaming --
-   -------------------------------
+   -------------------------------------
+   -- Expand_SPARK_Potential_Renaming --
+   -------------------------------------
 
-   procedure Expand_Potential_Renaming (N : Node_Id) is
-      Id     : constant Entity_Id  := Entity (N);
+   procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
       Loc    : constant Source_Ptr := Sloc (N);
+      Ren_Id : constant Entity_Id  := Entity (N);
       Typ    : constant Entity_Id  := Etype (N);
-      Ren_Id : Node_Id;
+      Obj_Id : Node_Id;
 
    begin
       --  Replace a reference to a renaming with the actual renamed object
 
-      if Ekind (Id) in Object_Kind then
-         Ren_Id := Renamed_Object (Id);
+      if Ekind (Ren_Id) in Object_Kind then
+         Obj_Id := Renamed_Object (Ren_Id);
 
-         if Present (Ren_Id) then
+         if Present (Obj_Id) then
 
             --  The renamed object is an entity when instantiating generics
             --  or inlining bodies. In this case the renaming is part of the
             --  mapping "prologue" which links actuals to formals.
 
-            if Nkind (Ren_Id) in N_Entity then
-               Rewrite (N, New_Occurrence_Of (Ren_Id, Loc));
+            if Nkind (Obj_Id) in N_Entity then
+               Rewrite (N, New_Occurrence_Of (Obj_Id, Loc));
 
             --  Otherwise the renamed object denotes a name
 
             else
-               Rewrite (N, New_Copy_Tree (Ren_Id));
+               Rewrite (N, New_Copy_Tree (Obj_Id));
                Reset_Analyzed_Flags (N);
             end if;
 
             Analyze_And_Resolve (N, Typ);
          end if;
       end if;
-   end Expand_Potential_Renaming;
+   end Expand_SPARK_Potential_Renaming;
 
 end Exp_SPARK;
Index: exp_spark.ads
===================================================================
--- exp_spark.ads	(revision 235481)
+++ exp_spark.ads	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2011-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2011-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- --
@@ -35,4 +35,8 @@
 
    procedure Expand_SPARK (N : Node_Id);
 
+   procedure Expand_SPARK_Potential_Renaming (N : Node_Id);
+   --  N must denote an N_Expanded_Name or N_Identifier. If N is a reference to
+   --  a renaming, replace N with the renamed object.
+
 end Exp_SPARK;
Index: sem.adb
===================================================================
--- sem.adb	(revision 235481)
+++ sem.adb	(working copy)
@@ -23,39 +23,40 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with Atree;    use Atree;
-with Debug;    use Debug;
-with Debug_A;  use Debug_A;
-with Elists;   use Elists;
-with Expander; use Expander;
-with Fname;    use Fname;
-with Ghost;    use Ghost;
-with Lib;      use Lib;
-with Lib.Load; use Lib.Load;
-with Nlists;   use Nlists;
-with Output;   use Output;
-with Restrict; use Restrict;
-with Sem_Attr; use Sem_Attr;
-with Sem_Aux;  use Sem_Aux;
-with Sem_Ch2;  use Sem_Ch2;
-with Sem_Ch3;  use Sem_Ch3;
-with Sem_Ch4;  use Sem_Ch4;
-with Sem_Ch5;  use Sem_Ch5;
-with Sem_Ch6;  use Sem_Ch6;
-with Sem_Ch7;  use Sem_Ch7;
-with Sem_Ch8;  use Sem_Ch8;
-with Sem_Ch9;  use Sem_Ch9;
-with Sem_Ch10; use Sem_Ch10;
-with Sem_Ch11; use Sem_Ch11;
-with Sem_Ch12; use Sem_Ch12;
-with Sem_Ch13; use Sem_Ch13;
-with Sem_Prag; use Sem_Prag;
-with Sem_Util; use Sem_Util;
-with Sinfo;    use Sinfo;
-with Stand;    use Stand;
-with Stylesw;  use Stylesw;
-with Uintp;    use Uintp;
-with Uname;    use Uname;
+with Atree;     use Atree;
+with Debug;     use Debug;
+with Debug_A;   use Debug_A;
+with Elists;    use Elists;
+with Exp_SPARK; use Exp_SPARK;
+with Expander;  use Expander;
+with Fname;     use Fname;
+with Ghost;     use Ghost;
+with Lib;       use Lib;
+with Lib.Load;  use Lib.Load;
+with Nlists;    use Nlists;
+with Output;    use Output;
+with Restrict;  use Restrict;
+with Sem_Attr;  use Sem_Attr;
+with Sem_Aux;   use Sem_Aux;
+with Sem_Ch2;   use Sem_Ch2;
+with Sem_Ch3;   use Sem_Ch3;
+with Sem_Ch4;   use Sem_Ch4;
+with Sem_Ch5;   use Sem_Ch5;
+with Sem_Ch6;   use Sem_Ch6;
+with Sem_Ch7;   use Sem_Ch7;
+with Sem_Ch8;   use Sem_Ch8;
+with Sem_Ch9;   use Sem_Ch9;
+with Sem_Ch10;  use Sem_Ch10;
+with Sem_Ch11;  use Sem_Ch11;
+with Sem_Ch12;  use Sem_Ch12;
+with Sem_Ch13;  use Sem_Ch13;
+with Sem_Prag;  use Sem_Prag;
+with Sem_Util;  use Sem_Util;
+with Sinfo;     use Sinfo;
+with Stand;     use Stand;
+with Stylesw;   use Stylesw;
+with Uintp;     use Uintp;
+with Uname;     use Uname;
 
 with Unchecked_Deallocation;
 
@@ -726,6 +727,21 @@
                   and then Etype (N) = Standard_Void_Type)
       then
          Expand (N);
+
+      --  Replace a reference to a renaming with the renamed object for SPARK.
+      --  In general this modification is performed by Expand_SPARK, however
+      --  certain constructs may not reach the resolution or expansion phase
+      --  and thus remain unchanged. The replacement is not performed when the
+      --  construct is overloaded as resolution must first take place. This is
+      --  also not done when analyzing a generic to preserve the original tree
+      --  and because the reference may become overloaded in the instance.
+
+      elsif GNATprove_Mode
+        and then Nkind_In (N, N_Expanded_Name, N_Identifier)
+        and then not Is_Overloaded (N)
+        and then not Inside_A_Generic
+      then
+         Expand_SPARK_Potential_Renaming (N);
       end if;
 
       Ghost_Mode := Save_Ghost_Mode;
