aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-04-24 11:59:50 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-05 11:54:04 +0200
commit7ad6799bccce274244e6a52c89d579e1588d1e9c (patch)
treec3669c4712c8d6667d9fc5ee655607616e358a03
parent5eb1dd3df297c30fccd4ad09a3a16b114eb4c5e0 (diff)
[sphinx] Replace remaining `@natural` by `@num`.
-rw-r--r--doc/sphinx/proof-engine/ltac.rst10
-rw-r--r--doc/sphinx/proof-engine/ssreflect-proof-language.rst10
2 files changed, 10 insertions, 10 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 86b178290..dc9add66f 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -547,7 +547,7 @@ Failing
:tacn:`fail` tactic will, however, succeed if all the goals have already been
solved.
- .. tacv:: fail @natural
+ .. tacv:: fail @num
The number is the failure level. If no level is specified, it defaults to 0.
The level is used by :tacn:`try`, :tacn:`repeat`, :tacn:`match goal` and the branching
@@ -555,14 +555,14 @@ Failing
(backtracking). If non zero, the current :tacn:`match goal` block, :tacn:`try`,
:tacn:`repeat`, or branching command is aborted and the level is decremented. In
the case of :n:`+`, a non-zero level skips the first backtrack point, even if
- the call to :n:`fail @natural` is not enclosed in a :n:`+` command,
+ the call to :n:`fail @num` is not enclosed in a :n:`+` command,
respecting the algebraic identity.
.. tacv:: fail {* message_token}
The given tokens are used for printing the failure message.
- .. tacv:: fail @natural {* message_token}
+ .. tacv:: fail @num {* message_token}
This is a combination of the previous variants.
@@ -573,7 +573,7 @@ Failing
.. tacv:: gfail {* message_token}
- .. tacv:: gfail @natural {* message_token}
+ .. tacv:: gfail @num {* message_token}
These variants fail with an error message or an error level even if
there are no goals left. Be careful however if Coq terms have to be
@@ -581,7 +581,7 @@ Failing
tactic into the goals, meaning that if there are no goals when it is
evaluated, a tactic call like :n:`let x:=H in fail 0 x` will succeed.
- .. exn:: Tactic Failure message (level @natural).
+ .. exn:: Tactic Failure message (level @num).
Timeout
~~~~~~~
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 977a5b8fa..8816c934a 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2157,10 +2157,10 @@ equivalent to:
More generally, the tactic:
-.. tacn:: @tactic; last @natural first
+.. tacn:: @tactic; last @num first
:name: last first
-where :token:`natural` is a |Coq| numeral, or and Ltac variable
+where :token:`num` is a |Coq| numeral, or an Ltac variable
denoting a |Coq|
numeral, having the value k. It rotates the n subgoals G1 , …, Gn
generated by tactic. The first subgoal becomes Gn + 1 − k and the
@@ -2168,7 +2168,7 @@ circular order of subgoals remains unchanged.
Conversely, the tactic:
-.. tacn:: @tactic; first @natural last
+.. tacn:: @tactic; first @num last
:name: first last
rotates the n subgoals G1 , …, Gn generated by tactic in order that
@@ -5322,11 +5322,11 @@ intro item see :ref:`introduction_ssr`
multiplier see :ref:`iteration_ssr`
-.. prodn:: occ_switch ::= { {? + %| - } {* @natural } }
+.. prodn:: occ_switch ::= { {? + %| - } {* @num } }
occur. switch see :ref:`occurrence_selection_ssr`
-.. prodn:: mult ::= {? @natural } @mult_mark
+.. prodn:: mult ::= {? @num } @mult_mark
multiplier see :ref:`iteration_ssr`