From 457cee4345ab4ad6b6624a6886841fd0b0739b2a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Jan 2020 08:18:49 +0100
Subject: Allow to rebind the old value of a mutable Ltac2 entry.

---
 test-suite/ltac2/rebind.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v
index e1c20a2059..6cec49de1e 100644
--- a/test-suite/ltac2/rebind.v
+++ b/test-suite/ltac2/rebind.v
@@ -32,3 +32,19 @@ Fail Ltac2 Set f := fun x => x.
 Ltac2 mutable g x := x.
 
 Ltac2 Set g := f.
+
+(* Rebinding with old values *)
+
+Ltac2 mutable qux () := Message.print (Message.of_string "Hello").
+
+Ltac2 Set qux as self := fun () => self (); self ().
+
+Ltac2 Eval qux ().
+
+Ltac2 Type rec nat := [O | S (nat)].
+
+Ltac2 mutable quz := O.
+
+Ltac2 Set quz as self := S self.
+
+Ltac2 Eval quz.
-- 
cgit v1.2.3


From 6cb24494fe8b6e945c6b6696134a6a42ecdab6ec Mon Sep 17 00:00:00 2001
From: Kenji Maillard
Date: Sun, 10 May 2020 15:14:42 +0200
Subject: Correcting ltac2's documentation on values turning test into proper
 check.

---
 test-suite/ltac2/rebind.v | 25 ++++++++++++++++++++-----
 1 file changed, 20 insertions(+), 5 deletions(-)

(limited to 'test-suite')

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)).
-- 
cgit v1.2.3


From ceb1f5676fa3fd5c1a0b06d45ec62626175d78aa Mon Sep 17 00:00:00 2001
From: Kenji Maillard
Date: Mon, 11 May 2020 23:10:03 +0200
Subject: More tests of rebinding Ltac2 definitions

---
 test-suite/ltac2/rebind.v | 76 +++++++++++++++++++++++++++++++++++------------
 1 file changed, 57 insertions(+), 19 deletions(-)

(limited to 'test-suite')

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))))))).
-- 
cgit v1.2.3