From 654b69cbeb55a0cab3c2328d73355ad2510d1a85 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 29 Oct 2015 14:21:25 +0100
Subject: Fixing another instance of bug #3267 in eauto, this time in the
 presence of hints modifying the context and of a "using" clause.

Incidentally opening Hints by default in debugger.
---
 test-suite/bugs/closed/3267.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3267.v b/test-suite/bugs/closed/3267.v
index 5ce1ddf0c4..8175d66ac7 100644
--- a/test-suite/bugs/closed/3267.v
+++ b/test-suite/bugs/closed/3267.v
@@ -34,3 +34,14 @@ Module d.
     debug eauto.
   Defined.
 End d.
+
+(* An other variant which was still failing in 8.5 beta2 *)
+
+Parameter A B : Prop.
+Axiom a:B.
+
+Hint Extern 1 => match goal with H:_ -> id _ |- _ => try (unfold id in H) end.
+Goal (B -> id A) -> A.
+intros.
+eauto using a.
+Abort.
-- 
cgit v1.2.3


From a3a17b514a2ffaba54cd182fdf27b7e84366ab44 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 29 Oct 2015 15:11:29 -0400
Subject: Handle side-effects of Vernacular commands inside proofs better, so
 that universes are declared correctly in the enclosing proofs evar_map's.

---
 test-suite/success/sideff.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 test-suite/success/sideff.v

(limited to 'test-suite')

diff --git a/test-suite/success/sideff.v b/test-suite/success/sideff.v
new file mode 100644
index 0000000000..3c0b81568a
--- /dev/null
+++ b/test-suite/success/sideff.v
@@ -0,0 +1,12 @@
+Definition idw (A : Type) := A.
+Lemma foobar : unit.
+Proof.
+  Require Import Program.
+  apply (const tt tt).
+Qed.
+
+Lemma foobar' : unit.
+  Lemma aux : forall A : Type, A -> unit.
+  Proof. intros. pose (foo := idw A). exact tt. Show Universes. Qed.
+  apply (@aux unit tt).
+Qed.
-- 
cgit v1.2.3