diff options
| author | Pierre Roux | 2020-09-08 10:41:03 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-09-11 22:20:28 +0200 |
| commit | 92bc869c2cec1ffb7e2d0bfcc6b64147718fbe87 (patch) | |
| tree | 89834f9ed7d88379f9284d93947b6f7d54cef1ff /doc/sphinx/proof-engine | |
| parent | 031cc2ba1a19a06766df85b8693c72f16fa62de6 (diff) | |
Turn integer into natural in several mlgs
Negative values had no meaning there.
Those were spotted by Hugo Herbelin while reviewing #12979 .
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 2a102adfcc..f18569c7fd 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -876,7 +876,7 @@ Print/identity tactic: idtac ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. tacn:: idtac {* {| @ident | @string | @integer } } +.. tacn:: idtac {* {| @ident | @string | @natural } } :name: idtac Leaves the proof unchanged and prints the given tokens. Strings and integers are printed diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index b4f32c6cbb..773e393eb6 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1159,7 +1159,7 @@ Match on values Notations --------- -.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @integer } := @ltac2_expr +.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @natural } := @ltac2_expr :name: Ltac2 Notation .. todo seems like name maybe should use lident rather than ident, considering: |