diff options
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: |