Correcting ltac2's documentation on values turning test into proper check.

2 files changed, 31 insertions, 9 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.
 
diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v
index 6cec49de1e..86c755363e 100644
--- a/test-suite/ltac2/rebind.v
+++ b/test-suite/ltac2/rebind.v
@@ -35,16 +35,31 @@ Ltac2 Set g := f.
 
 (* Rebinding with old values *)
 
-Ltac2 mutable qux () := Message.print (Message.of_string "Hello").
+Ltac2 Type rec nat := [O | S (nat)].
 
-Ltac2 Set qux as self := fun () => self (); self ().
+Ltac2 rec nat_eq n m :=
+  match n with
+  | O => match m with | O => true | S _ => false end
+  | S n => match m with | O => false | S m => nat_eq n m end
+  end.
 
-Ltac2 Eval qux ().
+Ltac2 Type exn ::= [ Assertion_failed ].
+
+Ltac2 assert_eq n m :=
+  match nat_eq n m with
+  | true => ()
+  | false => Control.throw Assertion_failed end.
+
+
+Ltac2 mutable qux n := S n.
+
+Ltac2 Set qux as self := fun n => self (self n).
+
+Ltac2 Eval assert_eq (qux O) (S (S O)).
 
-Ltac2 Type rec nat := [O | S (nat)].
 
 Ltac2 mutable quz := O.
 
 Ltac2 Set quz as self := S self.
 
-Ltac2 Eval quz.
+Ltac2 Eval (assert_eq quz (S O)).