diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 68f15b73b60..c7e1696b86e 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,11 @@
+2014-07-30  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch5.adb: Improve error recovery.
+	* inline.adb (Build_Body_To_Inline): Set Full_Analysis to false
+	before analyzing the body, so that in GNATprove mode there is
+	no light expansion. Whatever expansion is required by SPARK will
+	be performed when analysing the inlined code.
+
 2014-07-30  Bob Duff  <duff@adacore.com>
 
 	* s-tataat.adb, s-tataat.ads, a-tasatt.adb: Minor comment fixes.
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 44cdec48aa4..b2ff243e38f 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -833,6 +833,7 @@ package body Inline is
 
    procedure Build_Body_To_Inline (N : Node_Id; Subp : Entity_Id) is
       Decl            : constant Node_Id := Unit_Declaration_Node (Subp);
+      Analysis_Status : constant Boolean := Full_Analysis;
       Original_Body   : Node_Id;
       Body_To_Analyze : Node_Id;
       Max_Size        : constant := 10;
@@ -1388,7 +1389,12 @@ package body Inline is
          Append (Body_To_Analyze, Declarations (N));
       end if;
 
+      --  The body to inline is pre-analyzed.  In GNATprove mode we must
+      --  disable full analysis as well so that light expansion does not
+      --  take place either, and name resolution is unaffected.
+
       Expander_Mode_Save_And_Set (False);
+      Full_Analysis := False;
       Remove_Pragmas;
 
       Analyze (Body_To_Analyze);
@@ -1398,6 +1404,7 @@ package body Inline is
       Remove (Body_To_Analyze);
 
       Expander_Mode_Restore;
+      Full_Analysis := Analysis_Status;
 
       --  Restore environment if previously saved
 
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 863d488ebd7..a961bb710ef 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -2841,6 +2841,13 @@ package body Sem_Ch5 is
             Error_Msg_Sloc := Sloc (Ent);
             Error_Msg_N ("implicit label declaration for & is hidden#", Id);
 
+            if Present (Homonym (Ent))
+              and then Ekind (Homonym (Ent)) = E_Label
+            then
+               Set_Entity (Id, Ent);
+               Set_Ekind (Ent, E_Loop);
+            end if;
+
          else
             Generate_Reference (Ent, N, ' ');
             Generate_Definition (Ent);