aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/sem_attr.adb
diff options
context:
space:
mode:
Diffstat (limited to 'gcc/ada/sem_attr.adb')
-rw-r--r--gcc/ada/sem_attr.adb6
1 files changed, 3 insertions, 3 deletions
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index f7fccfb..e5a5b05 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -4379,13 +4379,13 @@ package body Sem_Attr is
-- enclosing subprogram. This is properly an expansion activity
-- but it has to be performed now to prevent out-of-order issues.
- -- This expansion is both harmful and not needed in Alfa mode, since
+ -- This expansion is both harmful and not needed in SPARK mode, since
-- the formal verification backend relies on the types of nodes
-- (hence is not robust w.r.t. a change to base type here), and does
-- not suffer from the out-of-order issue described above. Thus, this
- -- expansion is skipped in Alfa mode.
+ -- expansion is skipped in SPARK mode.
- if not Is_Entity_Name (P) and then not Alfa_Mode then
+ if not Is_Entity_Name (P) and then not SPARK_Mode then
P_Type := Base_Type (P_Type);
Set_Etype (N, P_Type);
Set_Etype (P, P_Type);