diff options
Diffstat (limited to 'test-suite/failure/subtyping.v')
| -rw-r--r-- | test-suite/failure/subtyping.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/failure/subtyping.v b/test-suite/failure/subtyping.v new file mode 100644 index 00000000..35fd2036 --- /dev/null +++ b/test-suite/failure/subtyping.v @@ -0,0 +1,21 @@ +(* A variant of bug #1302 that must fail *) + +Module Type T. + + Parameter A : Type. + + Inductive L : Prop := + | L0 + | L1 : (A -> Prop) -> L. + +End T. + +Module TT : T. + + Parameter A : Type. + + Inductive L : Type := + | L0 + | L1 : (A -> Prop) -> L. + +End TT. |