diff options
Diffstat (limited to 'test-suite/failure/subtyping.v')
| -rw-r--r-- | test-suite/failure/subtyping.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/failure/subtyping.v b/test-suite/failure/subtyping.v index 35fd2036..127da851 100644 --- a/test-suite/failure/subtyping.v +++ b/test-suite/failure/subtyping.v @@ -4,17 +4,17 @@ Module Type T. Parameter A : Type. - Inductive L : Prop := + Inductive L : Prop := | L0 | L1 : (A -> Prop) -> L. End T. -Module TT : T. +Module TT : T. Parameter A : Type. - Inductive L : Type := + Inductive L : Type := | L0 | L1 : (A -> Prop) -> L. |