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