Add regression tests for 3188 and 3265

2 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3188.v b/test-suite/bugs/closed/3188.v
new file mode 100644
index 000000000..011760267
--- /dev/null
+++ b/test-suite/bugs/closed/3188.v
@@ -0,0 +1,22 @@
+(* File reduced by coq-bug-finder from 1656 lines to 221 lines to 26 lines to 7 lines. *)
+
+Module Long.
+  Require Import Coq.Classes.RelationClasses.
+
+  Hint Extern 0 => apply reflexivity : typeclass_instances.
+  Hint Extern 1 => symmetry.
+
+  Lemma foo : exists m' : Type, True.
+    intuition. (* Anomaly: Uncaught exception Not_found. Please report. *)
+  Abort.
+End Long.
+
+Module Short.
+  Require Import Coq.Classes.RelationClasses.
+
+  Hint Extern 0 => apply reflexivity : typeclass_instances.
+
+  Lemma foo : exists m' : Type, True.
+    try symmetry. (* Anomaly: Uncaught exception Not_found. Please report. *)
+  Abort.
+End Short.
diff --git a/test-suite/bugs/closed/3265.v b/test-suite/bugs/closed/3265.v
new file mode 100644
index 000000000..269c7b741
--- /dev/null
+++ b/test-suite/bugs/closed/3265.v
@@ -0,0 +1,6 @@
+Require Import Setoid.
+Hint Extern 0 => apply reflexivity : typeclass_instances.
+Goal forall (B : Type) (P : B -> Prop), exists y : B, P y.
+  intros.
+  try reflexivity. (* Anomaly: Uncaught exception Not_found. Please report. *)
+Abort.