The preferred casing is "GNATprove", i.e. "GNAT" in upper-case and
"prove" in lower-case.
Tested on x86_64-pc-linux-gnu, committed on trunk
2020-06-17 Piotr Trojanek <troja...@adacore.com>
gcc/ada/
* doc/gnat_rm/implementation_defined_pragmas.rst, lib-writ.ads,
par-prag.adb, sem_ch12.adb, sem_ch8.adb, sem_prag.adb: Fix
casing of GNATprove.
* gnat_rm.texi: Regenerate.--- gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
+++ gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
@@ -7421,7 +7421,7 @@ Syntax:
DETAILS ::= static_string_EXPRESSION
DETAILS ::= On | Off, static_string_EXPRESSION
- TOOL_NAME ::= GNAT | GNATProve
+ TOOL_NAME ::= GNAT | GNATprove
REASON ::= Reason => STRING_LITERAL {& STRING_LITERAL}
--- gcc/ada/gnat_rm.texi
+++ gcc/ada/gnat_rm.texi
@@ -21,7 +21,7 @@
@copying
@quotation
-GNAT Reference Manual , May 05, 2020
+GNAT Reference Manual , May 13, 2020
AdaCore
@@ -8902,7 +8902,7 @@ DETAILS ::= On | Off, local_NAME
DETAILS ::= static_string_EXPRESSION
DETAILS ::= On | Off, static_string_EXPRESSION
-TOOL_NAME ::= GNAT | GNATProve
+TOOL_NAME ::= GNAT | GNATprove
REASON ::= Reason => STRING_LITERAL @{& STRING_LITERAL@}
@end example
--- gcc/ada/lib-writ.ads
+++ gcc/ada/lib-writ.ads
@@ -1051,7 +1051,7 @@ package Lib.Writ is
procedure Write_ALI (Object : Boolean);
-- This procedure writes the library information for the current main unit
-- The Object parameter is true if an object file is created, and false
- -- otherwise. Note that the pseudo-object file generated in GNATProve mode
+ -- otherwise. Note that the pseudo-object file generated in GNATprove mode
-- does count as an object file from this point of view.
--
-- Note: in the case where we are not generating code (-gnatc mode), this
--- gcc/ada/par-prag.adb
+++ gcc/ada/par-prag.adb
@@ -1109,7 +1109,7 @@ begin
-- DETAILS ::= static_string_EXPRESSION
-- DETAILS ::= On | Off, static_string_EXPRESSION
- -- TOOL_NAME ::= GNAT | GNATProve
+ -- TOOL_NAME ::= GNAT | GNATprove
-- REASON ::= Reason => STRING_LITERAL {& STRING_LITERAL}
--- gcc/ada/sem_ch12.adb
+++ gcc/ada/sem_ch12.adb
@@ -1718,7 +1718,7 @@ package body Sem_Ch12 is
Assoc_List);
-- For a defaulted in_parameter, create an entry in the
- -- the list of defaulted actuals, for GNATProve use. Do
+ -- the list of defaulted actuals, for GNATprove use. Do
-- not included these defaults for an instance nested
-- within a generic, because the defaults are also used
-- in the analysis of the enclosing generic, and only
@@ -1928,7 +1928,7 @@ package body Sem_Ch12 is
end if;
-- If this is a nested generic, preserve default for later
- -- instantiations. We do this as well for GNATProve use,
+ -- instantiations. We do this as well for GNATprove use,
-- so that the list of generic associations is complete.
if No (Match) and then Box_Present (Formal) then
--- gcc/ada/sem_ch8.adb
+++ gcc/ada/sem_ch8.adb
@@ -7162,10 +7162,10 @@ package body Sem_Ch8 is
-- is an array type we may already have a usable subtype for it, so we
-- can use it rather than generating a new one, because the bounds
-- will be the values of the discriminants and not discriminant refs.
- -- This simplifies value tracing in GNATProve. For consistency, both
+ -- This simplifies value tracing in GNATprove. For consistency, both
-- the entity name and the subtype come from the constrained component.
- -- This is only used in GNATProve mode: when generating code it may be
+ -- This is only used in GNATprove mode: when generating code it may be
-- necessary to create an itype in the scope of use of the selected
-- component, e.g. in the context of a expanded record equality.
--- gcc/ada/sem_prag.adb
+++ gcc/ada/sem_prag.adb
@@ -25258,7 +25258,7 @@ package body Sem_Prag is
-- DETAILS ::= static_string_EXPRESSION
-- DETAILS ::= On | Off, static_string_EXPRESSION
- -- TOOL_NAME ::= GNAT | GNATProve
+ -- TOOL_NAME ::= GNAT | GNATprove
-- REASON ::= Reason => STRING_LITERAL {& STRING_LITERAL}
