From 9304f93c18485965af1507be71cf0a86d1758d4b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 11 Dec 2018 14:05:02 +0100
Subject: Tests for #4509, #6202 which happen to be fixed (was a lost of evars
 in shelf).

---
 test-suite/bugs/closed/bug_4509.v | 11 +++++++++++
 test-suite/bugs/closed/bug_6202.v | 11 +++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_4509.v
 create mode 100644 test-suite/bugs/closed/bug_6202.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/bug_4509.v b/test-suite/bugs/closed/bug_4509.v
new file mode 100644
index 0000000000..ceae7c5fc3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4509.v
@@ -0,0 +1,11 @@
+(* Was solved at some time, suspectingly in PR #6328 *)
+
+Goal exists n, n > 1.
+Proof.
+  unshelve eexists. (*2 goals, as expected*)
+  Undo.
+  unshelve (eexists; instantiate (1:=ltac:(idtac))). (*only 1 goal*)
+  shelve.
+  Undo.
+  2:unshelve instantiate (1:=_).
+Abort.
diff --git a/test-suite/bugs/closed/bug_6202.v b/test-suite/bugs/closed/bug_6202.v
new file mode 100644
index 0000000000..899260f59a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_6202.v
@@ -0,0 +1,11 @@
+(* This was fixed at some time, suspectingly in PR #6328 *)
+
+Inductive foo := F (a : forall var : Type -> Type, unit -> var unit) (_ : a = a).
+Goal foo.
+  eexists (fun var => fun u : unit => ltac:(clear u)).
+  shelve.
+  Unshelve.
+  all:[ > | ].
+  shelve.
+  Fail Grab Existential Variables.
+Abort.
-- 
cgit v1.2.3