diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-17 14:47:50 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-17 14:47:50 +0000 |
commit | e4dfd24e4a4d4251c79694d82b1aa860657ee6dc (patch) | |
tree | 5090fdfb3c6ae959fc2e3c0c7de451e067c866bd /test-suite/failure/subtyping.v | |
parent | 73b7f84df37666066fc6cf9cec0dba9e744c8f08 (diff) |
Correction bug #1302
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9494 85f007b7-540e-0410-9357-904b9bb8a0f7
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 000000000..35fd20369 --- /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. |