Ces fichiers repassent (y restait un bug dans l'inférence du prédicat)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2095 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 3 insertions, 5 deletions

diff --git a/test-suite/ideal-features/Case5.v b/test-suite/success/Case5.v
index d703286f9..fe49cdf95 100644
--- a/test-suite/ideal-features/Case5.v
+++ b/test-suite/success/Case5.v
@@ -1,5 +1,4 @@
 
-Reset ff.
 Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m).
 Parameter discr_r : (n:nat) ~(O=(S n)).
 Parameter discr_l : (n:nat) ~((S n)=O).
diff --git a/test-suite/ideal-features/Cases.v b/test-suite/success/Cases.v
index 313f8f74a..313f8f74a 100644
--- a/test-suite/ideal-features/Cases.v
+++ b/test-suite/success/Cases.v
diff --git a/test-suite/ideal-features/CasesDep.v b/test-suite/success/CasesDep.v
index 3a0c36b6d..0108c1e94 100644
--- a/test-suite/ideal-features/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -221,15 +221,15 @@ end.
 
 
 
-Fixpoint equalT [t1:TERM]:TERM->Prop :=
+Definition equalT [t1:TERM]:TERM->Prop :=
 [t2:TERM] 
  Cases t1 t2 of 
    (var  v1)        (var v2)    => True
  | (oper op1 l1)  (oper op2 l2) => False
  |  _                   _       => False 
- end
+ end.
 
-with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop :=
+Definition EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop :=
 [n2:posint][l2:(LTERM n2)]
  Cases l1 l2 of
     nil                 nil             => True 
@@ -239,7 +239,6 @@ end.
 
 
 Reset equalT.
-Reset EqListT.
 (* ------------------------------------------------------------------*)
 (*          Initial exemple (without patterns)                       *)
 (*-------------------------------------------------------------------*)