diff options
| author | Gaëtan Gilbert | 2020-08-28 15:22:26 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-28 15:22:26 +0200 |
| commit | 0b4c7edc03fda831a746e5a34418e948d19c9c62 (patch) | |
| tree | 5615c9909861433c354323fec8ed8cba2ed5da3c | |
| parent | 911f33f0a0ff648082d329841388f59e8cecf231 (diff) | |
Add test for past anomaly
Close #5703
I have no idea when this got fixed.
| -rw-r--r-- | test-suite/bugs/closed/bug_5703.v | 9 |
1 files changed, 9 insertions, 0 deletions
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. |