Index: lib-xref-spark_specific.adb
===================================================================
--- lib-xref-spark_specific.adb	(revision 210697)
+++ lib-xref-spark_specific.adb	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2011-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2011-2014, 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- --
@@ -23,10 +23,9 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with SPARK_Xrefs;     use SPARK_Xrefs;
-with Einfo;           use Einfo;
-with Nmake;           use Nmake;
-with Put_SPARK_Xrefs;
+with SPARK_Xrefs; use SPARK_Xrefs;
+with Einfo;       use Einfo;
+with Nmake;       use Nmake;
 
 with GNAT.HTable;
 
@@ -972,7 +971,9 @@
    -- Enclosing_Subprogram_Or_Package --
    -------------------------------------
 
-   function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id is
+   function Enclosing_Subprogram_Or_Library_Package
+     (N : Node_Id) return Entity_Id
+   is
       Result : Entity_Id;
 
    begin
@@ -990,13 +991,27 @@
       while Present (Result) loop
          case Nkind (Result) is
             when N_Package_Specification =>
-               Result := Defining_Unit_Name (Result);
-               exit;
 
+               --  Only return a library-level package
+
+               if Is_Library_Level_Entity (Defining_Entity (Result)) then
+                  Result := Defining_Entity (Result);
+                  exit;
+               else
+                  Result := Parent (Result);
+               end if;
+
             when N_Package_Body =>
-               Result := Defining_Unit_Name (Result);
-               exit;
 
+               --  Only return a library-level package
+
+               if Is_Library_Level_Entity (Defining_Entity (Result)) then
+                  Result := Defining_Entity (Result);
+                  exit;
+               else
+                  Result := Parent (Result);
+               end if;
+
             when N_Subprogram_Specification =>
                Result := Defining_Unit_Name (Result);
                exit;
@@ -1045,7 +1060,7 @@
       end if;
 
       return Result;
-   end Enclosing_Subprogram_Or_Package;
+   end Enclosing_Subprogram_Or_Library_Package;
 
    -----------------
    -- Entity_Hash --
@@ -1107,7 +1122,7 @@
                Create_Heap;
             end if;
 
-            Ref_Scope := Enclosing_Subprogram_Or_Package (N);
+            Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
 
             Deref.Ent := Heap;
             Deref.Loc := Loc;
Index: lib-xref.ads
===================================================================
--- lib-xref.ads	(revision 210697)
+++ lib-xref.ads	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1998-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 1998-2014, 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- --
@@ -624,8 +624,12 @@
 
    package SPARK_Specific is
 
-      function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id;
-      --  Return the closest enclosing subprogram of package
+      function Enclosing_Subprogram_Or_Library_Package
+        (N : Node_Id) return Entity_Id;
+      --  Return the closest enclosing subprogram of package. Only return a
+      --  library level package. If the package is enclosed in a subprogram,
+      --  return the subprogram. This ensures that GNATprove can distinguish
+      --  local variables from global variables.
 
       procedure Generate_Dereference
         (N   : Node_Id;
Index: lib-xref.adb
===================================================================
--- lib-xref.adb	(revision 210697)
+++ lib-xref.adb	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1998-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 1998-2014, 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- --
@@ -1029,8 +1029,10 @@
             Ref := Sloc (Nod);
             Def := Sloc (Ent);
 
-            Ref_Scope := SPARK_Specific.Enclosing_Subprogram_Or_Package (Nod);
-            Ent_Scope := SPARK_Specific.Enclosing_Subprogram_Or_Package (Ent);
+            Ref_Scope :=
+              SPARK_Specific.Enclosing_Subprogram_Or_Library_Package (Nod);
+            Ent_Scope :=
+              SPARK_Specific.Enclosing_Subprogram_Or_Library_Package (Ent);
 
             --  Since we are reaching through renamings in SPARK mode, we may
             --  end up with standard constants. Ignore those.