[Ada] Fix casing from GNATProve to GNATprove

2020-06-17  Piotr Trojanek  <trojanek@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.

diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
index e9e4958..e5ef967 100644 (file)
--- a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
+++ b/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}
 

diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index f012e75..8aa446e 100644 (file)
--- a/gcc/ada/gnat_rm.texi
+++ b/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

diff --git a/gcc/ada/lib-writ.ads b/gcc/ada/lib-writ.ads
index 5fd2308..e7f2e3f 100644 (file)
--- a/gcc/ada/lib-writ.ads
+++ b/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

diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index db6808d..0e5a32b 100644 (file)
--- a/gcc/ada/par-prag.adb
+++ b/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}
 

diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 2240b7e..a0b529d 100644 (file)
--- a/gcc/ada/sem_ch12.adb
+++ b/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

diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index 069341c..b189a52 100644 (file)
--- a/gcc/ada/sem_ch8.adb
+++ b/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.
 

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index f3f0aff..410a653 100644 (file)
--- a/gcc/ada/sem_prag.adb
+++ b/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}