diff options
| -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)). +*) |