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/Inversion.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/Inversion.v')
| -rw-r--r-- | test-suite/success/Inversion.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 96ac86830..c28e04eb7 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -13,3 +13,4 @@ Definition Psi00 : (nat -> Prop) := [n:nat] False. Definition Psi0 : (T O) := Psi00. Lemma Inversion_RO : (l:nat)(R O Psi0 l) -> (Psi00 l). Inversion 1. +Abort. |