diff options
| author | Kenji Maillard | 2020-05-10 15:14:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-11 13:24:58 +0200 |
| commit | 6cb24494fe8b6e945c6b6696134a6a42ecdab6ec (patch) | |
| tree | c76e720b6615594638367a802cc06bf0a86860fe /doc | |
| parent | ead129a76cb3ceb656b60556bf10f38c667ce45a (diff) | |
Correcting ltac2's documentation on values turning test into proper check.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 0eb7ac6bb2..2ec1d0521e 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -213,14 +213,21 @@ There is dedicated syntax for list and array literals. Ltac Definitions ~~~~~~~~~~~~~~~~ -.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_term +.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_value :name: Ltac2 This command defines a new global Ltac2 value. - For semantic reasons, the body of the Ltac2 definition must be a syntactical - value, that is, a function, a constant or a pure constructor recursively applied to - values. + The body of an Ltac2 definition is required to be a syntactical value + that is, a function, a constant, a pure constructor recursively applied to + values or a (non-recursive) let binding of a value in a value. + + .. productionlist:: coq + ltac2_value: fun `ltac2_var` => `ltac2_term` + : `ltac2_qualid` + : `ltac2_constructor` `ltac2_value` ... `ltac2_value` + : `ltac2_var` + : let `ltac2_var` := `ltac2_value` in `ltac2_value` If ``rec`` is set, the tactic is expanded into a recursive binding. |