[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 e9e49588021cd38013de0af250356cbadd861327..e5ef96752292bb2aff20a8b10c8b7c5743a1421d 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 f012e754f1ed40a4f519e96c10a046c93a60abce..8aa446e82a6b6657ef5430f5990ba26a88958f5d 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 5fd2308082dd12c569f36f71a644d45fc7a44973..e7f2e3fb08cad415e8459d8ea194723741b94614 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 db6808db3ed30d2cddcb9ab1786801cae08c4c17..0e5a32b62731ad7e9c2c805ae571aad58f8d124c 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 2240b7e24d2a148fc4046bc80470ab9212b80b7c..a0b529db88709ac4ee935a67d68baf0351383494 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 069341c0dcbbafc8e5ccbb4ba188e3ad8ef2bc84..b189a52db21da044e77952db8b660a407aff67b1 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 f3f0affb0cae8061f362967ba10d62a7bf622f4c..410a65365c2eaeb2dff769ea5509fafb72a84f7e 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}