ada: Fix regression under GNATProve mode

This patch fixes a regression recently introduced compiling
code under GNATprove mode.

gcc/ada/ChangeLog:

	* sem_res.adb (Resolve_Declare_Expression): Do not create a
	transient scope under GNATprove mode.

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 3af928ee1e2b9dc0653f1c8b4f8594ce3be15c4d..33148e935a26a6b8fd65963a8bf69f28bddfb48f 100644 (file)
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7775,6 +7775,7 @@ package body Sem_Res is
       --  be needed, we assume the worst case.
 
       if not Preanalysis_Active
+        and then not GNATprove_Mode
         and then (Requires_Transient_Scope (Typ)
                     or else Has_Sec_Stack_Call (Expr))
       then