ada: Fix breakage of GNATprove introduced by latest change

gcc/ada/ChangeLog:

	* sem_aggr.adb (Resolve_Aggr_Expr): Always perform a full analysis
	of the expression in SPARK mode.

diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb
index 8cc00ad3b27a54d6ec63e194e472929fe8d36ef1..3a82e6620c5e914d85ea30abdb13889b1b7221dc 100644 (file)
--- a/gcc/ada/sem_aggr.adb
+++ b/gcc/ada/sem_aggr.adb
@@ -2057,13 +2057,14 @@ package body Sem_Aggr is
             --  In an iterated context, preanalyze a copy of the expression to
             --  verify legality. We use a copy because the expression will be
             --  analyzed anew when the enclosing aggregate is expanded and the
-            --  construct is rewritten as a loop with a new index variable.
+            --  construct is rewritten as a loop with a new iteration variable.
+            --  This does not apply to SPARK mode, where expansion is skipped.
 
             --  If the parent is a component association, we also temporarily
             --  point its Expression field to the copy, because analysis may
             --  expect this invariant to hold.
 
-            if Iterated_Expr then
+            if Iterated_Expr and then not GNATprove_Mode then
                declare
                   In_Assoc : constant Boolean :=
                     Nkind (Parent (Expr)) in N_Component_Association