From 2b4517cf85432d68e53ac46815309fd8068a40ad Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 28 Aug 2016 19:43:00 +0200
Subject: Fix bug #4764: Syntactic notation externalization breaks.

---
 test-suite/bugs/closed/4764.v | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 test-suite/bugs/closed/4764.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4764.v b/test-suite/bugs/closed/4764.v
new file mode 100644
index 0000000000..e545cc1b71
--- /dev/null
+++ b/test-suite/bugs/closed/4764.v
@@ -0,0 +1,5 @@
+Notation prop_fun x y := (fun (x : Prop) => y).
+Definition foo := fun (p : Prop) => p.
+Definition bar := fun (_ : Prop) => O.
+Print foo.
+Print bar.
-- 
cgit v1.2.3


From 44ada644ef50563aa52cfcd7717d44bde29e5a20 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Aug 2016 17:37:27 +0200
Subject: Fix bug #3920: eapply masks an hypothesis name.

The problem came from the fact that the legacy beta-reduction occurring
after a rewrite was wrongly applied to the side-conditions of the
rewriting step. We restrict it to the correct goal in this patch.
---
 test-suite/bugs/closed/3920.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/3920.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3920.v b/test-suite/bugs/closed/3920.v
new file mode 100644
index 0000000000..a4adb23cc2
--- /dev/null
+++ b/test-suite/bugs/closed/3920.v
@@ -0,0 +1,7 @@
+Require Import Setoid.
+Axiom P : nat -> Prop.
+Axiom P_or : forall x y, P (x + y) <-> P x \/ P y.
+Lemma foo (H : P 3) : False.
+eapply or_introl in H.
+erewrite <- P_or in H.
+(* Error: No such hypothesis: H *)
-- 
cgit v1.2.3


From 4582ed1c8f0620941a3c296941b1dc808c95d7fe Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Aug 2016 18:47:45 +0200
Subject: Fix bug #4893: not_evar: unexpected failure in 8.5pl1.

---
 test-suite/bugs/closed/4893.v | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 test-suite/bugs/closed/4893.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4893.v b/test-suite/bugs/closed/4893.v
new file mode 100644
index 0000000000..9a35bcf954
--- /dev/null
+++ b/test-suite/bugs/closed/4893.v
@@ -0,0 +1,4 @@
+Goal True.
+evar (P: Prop).
+assert (H : P); [|subst P]; [exact I|].
+let T := type of H in not_evar T.
-- 
cgit v1.2.3


From 12268bef28dea57fdbe29dc87d26ef453ad5cfed Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 31 Aug 2016 11:32:28 +0200
Subject: Fix bug #5043: [Admitted] lemmas pick up section variables.

We add a flag Keep Admitted Variables that allows to recover the legacy
v8.4 behaviour of admitted lemmas. The statement of such lemmas did not
depend on the current context variables.
---
 test-suite/bugs/closed/5043.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/bugs/closed/5043.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/5043.v b/test-suite/bugs/closed/5043.v
new file mode 100644
index 0000000000..4e6a0f878f
--- /dev/null
+++ b/test-suite/bugs/closed/5043.v
@@ -0,0 +1,8 @@
+Unset Keep Admitted Variables.
+
+Section a.
+  Context (x : Type).
+  Definition foo : Type.
+  Admitted.
+End a.
+Check foo : Type.
-- 
cgit v1.2.3