diff options
| author | Gaëtan Gilbert | 2020-11-11 16:13:56 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-13 13:44:06 +0100 |
| commit | 76483168ec6a27a1cf456aa8ead92273e2c74bfd (patch) | |
| tree | e722a80d1429b5966b855a1b02efd7c467d3578a /test-suite | |
| parent | 51e759fb2ff92dd89ab4823ddea3ea81be7f8046 (diff) | |
Fix incorrect "avoid" set in globenv extra data
Fix #13348
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_13348.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_13348.v b/test-suite/bugs/closed/bug_13348.v new file mode 100644 index 0000000000..d3d5d3e5b4 --- /dev/null +++ b/test-suite/bugs/closed/bug_13348.v @@ -0,0 +1,10 @@ +Generalizable All Variables. + +Class Inhabited (A : Type) : Type := populate { inhabitant : A }. +Arguments populate {_} _. + +Set Mangle Names. +Axioms _0 _1 _2 : Prop. + +Instance impl_inhabited {A} {B} {_3:Inhabited B} : Inhabited (A -> B) + := populate (fun _ => inhabitant). |
