From 07d63e1333dc73eda3e49e904ff8df6e7f62fa79 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 10 Apr 2015 16:14:09 +0200
Subject: Test for bug #3199.

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

diff --git a/test-suite/bugs/closed/3199.v b/test-suite/bugs/closed/3199.v
new file mode 100644
index 0000000000..08bf62493d
--- /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.
-- 
cgit v1.2.3