[Ada] Fix inconsistent documentation for the Contract_Cases pragma
authorPiotr Trojanek <trojanek@adacore.com>
Thu, 24 May 2018 13:04:44 +0000 (13:04 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Thu, 24 May 2018 13:04:44 +0000 (13:04 +0000)
This patch propagates the renaming from "condition" to "case guard" in the
contract grammar to the paragraphs that describe the pragma semantics.

2018-05-24  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

* doc/gnat_rm/implementation_defined_pragmas.rst (Contract_Cases):
Change "condition" to "case guard" after renaming in the contract
grammar.
* gnat_rm.texi: Regenerate.

From-SVN: r260647

gcc/ada/ChangeLog
gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
gcc/ada/gnat_rm.texi

index 50c886d4e6f3e737287596ceb9a84c1b32ade3f2..219fa8bfe97de7afe17d2513a5ce53c944956e86 100644 (file)
@@ -1,3 +1,10 @@
+2018-05-24  Piotr Trojanek  <trojanek@adacore.com>
+
+       * doc/gnat_rm/implementation_defined_pragmas.rst (Contract_Cases):
+       Change "condition" to "case guard" after renaming in the contract
+       grammar.
+       * gnat_rm.texi: Regenerate.
+
 2018-05-24  Hristian Kirtchev  <kirtchev@adacore.com>
 
        * exp_util.adb (Expand_Static_Predicates_In_Choices): Indicate that the
index 73d7db898732f5649b21dac61bb1a6545cbb3ead..353a9a5f346120f29ed8ba32548af589162c9a64 100644 (file)
@@ -1173,9 +1173,9 @@ are equivalent to
   pragma Postcondition (if C2 then Pred2);
 
 
-The precondition ensures that one and only one of the conditions is
+The precondition ensures that one and only one of the case guards is
 satisfied on entry to the subprogram.
-The postcondition ensures that for the condition that was True on entry,
+The postcondition ensures that for the case guard that was True on entry,
 the corrresponding consequence is True on exit. Other consequence expressions
 are not evaluated.
 
@@ -1190,13 +1190,13 @@ expressed as contract cases:
 The placement and visibility rules for ``Contract_Cases`` pragmas are
 identical to those described for preconditions and postconditions.
 
-The compiler checks that boolean expressions given in conditions and
-consequences are valid, where the rules for conditions are the same as
+The compiler checks that boolean expressions given in case guards and
+consequences are valid, where the rules for case guards are the same as
 the rule for an expression in ``Precondition`` and the rules for
 consequences are the same as the rule for an expression in
 ``Postcondition``. In particular, attributes ``'Old`` and
 ``'Result`` can only be used within consequence expressions.
-The condition for the last contract case may be ``others``, to denote
+The case guard for the last contract case may be ``others``, to denote
 any case not captured by the previous cases. The
 following is an example of use within a package spec:
 
@@ -1214,7 +1214,7 @@ following is an example of use within a package spec:
 
 
 The meaning of contract cases is that only one case should apply at each
-call, as determined by the corresponding condition evaluating to True,
+call, as determined by the corresponding case guard evaluating to True,
 and that the consequence for this case should hold when the subprogram
 returns.
 
index a0c75753f045cf27b3d2eb20cf675b15fc1b478d..ac29d3f6af8efd05c3b10cd9753a4ca606c7fa7f 100644 (file)
@@ -21,7 +21,7 @@
 
 @copying
 @quotation
-GNAT Reference Manual , Apr 23, 2018
+GNAT Reference Manual , Apr 24, 2018
 
 AdaCore
 
@@ -2556,9 +2556,9 @@ pragma Postcondition (if C1 then Pred1);
 pragma Postcondition (if C2 then Pred2);
 @end example
 
-The precondition ensures that one and only one of the conditions is
+The precondition ensures that one and only one of the case guards is
 satisfied on entry to the subprogram.
-The postcondition ensures that for the condition that was True on entry,
+The postcondition ensures that for the case guard that was True on entry,
 the corrresponding consequence is True on exit. Other consequence expressions
 are not evaluated.
 
@@ -2572,13 +2572,13 @@ pragma Contract_Cases (P => Q);
 The placement and visibility rules for @code{Contract_Cases} pragmas are
 identical to those described for preconditions and postconditions.
 
-The compiler checks that boolean expressions given in conditions and
-consequences are valid, where the rules for conditions are the same as
+The compiler checks that boolean expressions given in case guards and
+consequences are valid, where the rules for case guards are the same as
 the rule for an expression in @code{Precondition} and the rules for
 consequences are the same as the rule for an expression in
 @code{Postcondition}. In particular, attributes @code{'Old} and
 @code{'Result} can only be used within consequence expressions.
-The condition for the last contract case may be @code{others}, to denote
+The case guard for the last contract case may be @code{others}, to denote
 any case not captured by the previous cases. The
 following is an example of use within a package spec:
 
@@ -2594,7 +2594,7 @@ end Math_Functions;
 @end example
 
 The meaning of contract cases is that only one case should apply at each
-call, as determined by the corresponding condition evaluating to True,
+call, as determined by the corresponding case guard evaluating to True,
 and that the consequence for this case should hold when the subprogram
 returns.