From b96e5090b18696dbd12040f8505139f3fc08047b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Mar 2004 09:47:56 +0000
Subject: Corrections

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5463 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Inversion.v | 2 +-
 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)).
+*)
-- 
cgit v1.2.3