diff options
| author | herbelin | 2004-03-12 09:47:56 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-12 09:47:56 +0000 |
| commit | b96e5090b18696dbd12040f8505139f3fc08047b (patch) | |
| tree | 3b560c090e99755a99f500415449c999b01d7a18 | |
| parent | cfbde631e375ed0ebc8016702bbf768f371b1c28 (diff) | |
Corrections
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5463 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | test-suite/success/Inversion.v | 2 | ||||
| -rw-r--r-- | test-suite/success/implicit.v | 4 |
2 files changed, 4 insertions, 2 deletions
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 3e5540d383..04b3953975 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -50,7 +50,7 @@ Lemma super_def : (I :Set)(e1, e2: (extension I)) Proof. Induction 1. Inversion 1; Auto. - Elim magic + Elim magic. Qed. (* Example from Norbert Schirmer on Coq-Club, Sep 2000 *) diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index 9f2837e373..c597f9bf89 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -26,4 +26,6 @@ Check [x](lhs ? ? (f x)). Check [x](!lhs ? ? (f x)). Notation "'rhs'" := snd. Check [x](rhs ? ? (f x)). -Check [x](!rhs ? ? (f x)). +(* V8 seulement +Check (fun x => @ rhs ? ? (f x)). +*) |