From 0b4c7edc03fda831a746e5a34418e948d19c9c62 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 28 Aug 2020 15:22:26 +0200
Subject: Add test for past anomaly

Close #5703

I have no idea when this got fixed.
---
 test-suite/bugs/closed/bug_5703.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_5703.v

diff --git a/test-suite/bugs/closed/bug_5703.v b/test-suite/bugs/closed/bug_5703.v
new file mode 100644
index 0000000000..c6e9eab9a7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5703.v
@@ -0,0 +1,9 @@
+Class A := {}.
+Instance a:A := {}.
+Hint Extern 0 A => abstract (exact a) : typeclass_instances.
+Lemma lem : A.
+Proof.
+  let a := constr:(_:A) in
+  let b := type of a in
+  exact a.
+Defined.
-- 
cgit v1.2.3