Imported Upstream version 8.5~beta1+dfsg

1 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3188.v b/test-suite/bugs/closed/3188.v
new file mode 100644
index 00000000..01176026
--- /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.