diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-19 23:05:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-19 23:05:10 +0000 |
| commit | d3950750f636057674c0ee527d5c05937faf90a2 (patch) | |
| tree | fcb75abc28ad2932409cc0fb89c512d0a74f8e9f /test-suite/success/univers.v | |
| parent | 326617c10cc2e63d71d09300e7de0c7f4ea18f33 (diff) | |
Il ne doit plus y avoir de preuves non terminées à la sortie du fichier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3538 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/univers.v')
| -rw-r--r-- | test-suite/success/univers.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index 28f9fe981..0a4b284f9 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -3,15 +3,17 @@ Definition Type2 := Type. Definition Type1 := Type : Type2. -Goal (True->Type1)->Type2. +Lemma lem1 : (True->Type1)->Type2. Intro H. Apply H. +Exact I. +Qed. -Lemma gg : (A:Type)(P:A->Type)(x:A)((y:A)(x==y)->(P y))->(P x). +Lemma lem2 : (A:Type)(P:A->Type)(x:A)((y:A)(x==y)->(P y))->(P x). Auto. Qed. -Lemma titi : (P:Prop)P. +Lemma lem3 : (P:Prop)P. Intro P ; Pattern P. -Apply gg. - +Apply lem2. +Abort. |