diff options
| author | Gaëtan Gilbert | 2018-03-01 14:32:04 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-03-01 14:33:28 +0100 |
| commit | 01cf21509667263c2067cb87e2b2f604c4f9cb1e (patch) | |
| tree | 8233b6fa643e289e98afe217931dd4558f81953e /test-suite | |
| parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) | |
Fix #6878: univ undefined for [with Definition] bad instance size.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/6878.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/6878.v b/test-suite/bugs/closed/6878.v new file mode 100644 index 0000000000..70f1b3127a --- /dev/null +++ b/test-suite/bugs/closed/6878.v @@ -0,0 +1,8 @@ + +Set Universe Polymorphism. +Module Type T. + Axiom foo : Prop. +End T. + +(** Used to anomaly *) +Fail Module M : T with Definition foo := Type. |