More tests of rebinding Ltac2 definitions

1 files changed, 57 insertions, 19 deletions

diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v
index 86c755363e..7b3a460c8c 100644
--- a/test-suite/ltac2/rebind.v
+++ b/test-suite/ltac2/rebind.v
@@ -15,25 +15,8 @@ Fail foo ().
 constructor.
 Qed.
 
-(** Not the right type *)
-Fail Ltac2 Set foo := 0.
-
-Ltac2 bar () := ().
-
-(** Cannot redefine non-mutable tactics *)
-Fail Ltac2 Set bar := fun _ => ().
-
-(** Subtype check *)
 
-Ltac2 mutable rec f x := f x.
-
-Fail Ltac2 Set f := fun x => x.
-
-Ltac2 mutable g x := x.
-
-Ltac2 Set g := f.
-
-(* Rebinding with old values *)
+(** Bindings are dynamic *)
 
 Ltac2 Type rec nat := [O | S (nat)].
 
@@ -50,6 +33,42 @@ Ltac2 assert_eq n m :=
   | true => ()
   | false => Control.throw Assertion_failed end.
 
+Ltac2 mutable x := O.
+Ltac2 y := x.
+Ltac2 Eval (assert_eq y O).
+Ltac2 Set x := (S O).
+Ltac2 Eval (assert_eq y (S O)).
+
+Ltac2 mutable quw := fun (n : nat) => O.
+Ltac2 Set quw := fun n =>
+  match n with
+  | O => O
+  | S n => S (S (quw n))
+  end.
+
+Ltac2 Eval (quw (S (S O))).
+
+(** Not the right type *)
+Fail Ltac2 Set foo := 0.
+
+Ltac2 bar () := ().
+
+(** Cannot redefine non-mutable tactics *)
+Fail Ltac2 Set bar := fun _ => ().
+
+(** Subtype check *)
+
+Ltac2 rec h x := h x.
+
+Ltac2 mutable f x := h x.
+Fail Ltac2 Set f := fun x => x.
+
+Ltac2 mutable g x := x.
+Ltac2 Set g := h.
+
+(** Rebinding with old values *)
+
+
 
 Ltac2 mutable qux n := S n.
 
@@ -57,9 +76,28 @@ Ltac2 Set qux as self := fun n => self (self n).
 
 Ltac2 Eval assert_eq (qux O) (S (S O)).
 
-
 Ltac2 mutable quz := O.
 
 Ltac2 Set quz as self := S self.
 
 Ltac2 Eval (assert_eq quz (S O)).
+
+Ltac2 rec addn n :=
+  match n with
+  | O => fun m => m
+  | S n => fun m => S (addn n m)
+
+  end.
+Ltac2 mutable rec quy n :=
+  match n with
+  | O => S O
+  | S n => S (quy n)
+  end.
+
+Ltac2 Set quy as self := fun n =>
+                           match n with
+                           | O => O
+                           | S n => addn (self n) (quy n)
+                           end.
+Ltac2 Eval (assert_eq (quy (S (S O))) (S (S (S O)))).
+Ltac2 Eval (assert_eq (quy (S (S (S O)))) (S (S (S (S (S (S O))))))).