Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3199.v b/test-suite/bugs/closed/3199.v
new file mode 100644
index 00000000..08bf6249
--- /dev/null
+++ b/test-suite/bugs/closed/3199.v
@@ -0,0 +1,18 @@
+Axiom P : nat -> Prop.
+Axiom admit : forall n : nat, P n -> P n -> n = S n.
+Axiom foo : forall n, P n.
+
+Create HintDb bar.
+Hint Extern 3 => symmetry : bar.
+Hint Resolve admit : bar.
+Hint Immediate foo : bar.
+
+Lemma qux : forall n : nat, n = S n.
+Proof.
+intros n.
+eauto with bar.
+Defined.
+
+Goal True.
+pose (e := eq_refl (qux 0)); unfold qux in e.
+match type of e with context [eq_sym] => fail 1 | _ => idtac end.