[Ada] Fix casing from GNATProve to GNATprove

--- 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}