Index: exp_ch5.adb
===================================================================
--- exp_ch5.adb	(revision 216063)
+++ exp_ch5.adb	(working copy)
@@ -2889,7 +2889,17 @@
               Statements =>  New_List (New_Loop)));
 
       Rewrite (N, New_Loop);
-      Analyze (New_Loop);
+
+      --  The loop parameter is declared by an object declaration, but within
+      --  the loop we must prevent user assignments to it, so we analyze the
+      --  declaration and reset the entity kind, before analyzing the rest of
+      --  the loop;
+
+      Analyze (Elmt_Decl);
+      Set_Ekind (Defining_Identifier (Elmt_Decl), E_Loop_Parameter);
+      Set_Assignment_OK (Name (Elmt_Ref));
+
+      Analyze (N);
    end Expand_Formal_Container_Element_Loop;
 
    -----------------------------
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 216063)
+++ sem_ch3.adb	(working copy)
@@ -3062,6 +3062,12 @@
             Error_Msg_N ("constant cannot be volatile", Obj_Id);
          end if;
 
+      --  The loop parameter in an element iterator over a formal container
+      --  is declared with an object declaration but no contracts apply.
+
+      elsif Ekind (Obj_Id) = E_Loop_Parameter then
+         null;
+
       else pragma Assert (Ekind (Obj_Id) = E_Variable);
 
          --  The following checks are only relevant when SPARK_Mode is on as