From 7ad6799bccce274244e6a52c89d579e1588d1e9c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 24 Apr 2018 11:59:50 +0200 Subject: [sphinx] Replace remaining `@natural` by `@num`. --- doc/sphinx/proof-engine/ltac.rst | 10 +++++----- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 10 +++++----- 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` -- cgit v1.2.3