diff options
author | 2001-11-21 00:16:11 +0000 | |
---|---|---|
committer | 2001-11-21 00:16:11 +0000 | |
commit | 207a70679aabff4a6a235b858a9814fed7cb5fe0 (patch) | |
tree | b7a58fc89139921d5a661919da77d974110ba71c /test-suite | |
parent | 3bd6c650480c842088dd8ab2d5397ad310a4e152 (diff) |
Sur la cumulativité dans les tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2223 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/success/univers.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v new file mode 100644 index 000000000..7bb3c363b --- /dev/null +++ b/test-suite/success/univers.v @@ -0,0 +1,17 @@ +(* This requires cumulativity *) + +Definition Type2 := Type. +Definition Type1 := Type : Type2. + +Goal (True->Type1)->Type2. +Intro H. +Apply H. + +Lemma gg : (A:Type)(P:A->Type)(x:A)((y:A)(x==y)->(P y))->(P x). +Auto. +Qed. + +Lemma titi : (P:Prop)P. +Intro P ; Pattern P. +Apply gg. +Qed. |