diff options
| author | Pierre-Marie Pédrot | 2020-08-28 18:28:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-28 18:28:33 +0200 |
| commit | bbe60065397e61162bc43b40aa1d58201b639b88 (patch) | |
| tree | bfc9351a4849d1b2687f02c29bd5e47149ddb747 | |
| parent | 511c280825ea30cb93fa00e47d487875a489ac2c (diff) | |
| parent | 0b4c7edc03fda831a746e5a34418e948d19c9c62 (diff) | |
Merge PR #12933: Add test for past anomaly
Reviewed-by: ppedrot
| -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. |