Adaptation des tests suite à la modification de Rewrite .. in (r9201)

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

1 files changed, 3 insertions, 9 deletions

diff --git a/test-suite/success/autorewritein.v b/test-suite/success/autorewritein.v
index 2f7d86dae..68f2f7ce7 100644
--- a/test-suite/success/autorewritein.v
+++ b/test-suite/success/autorewritein.v
@@ -12,17 +12,11 @@ Proof.
   autorewrite with base0 in H using try (apply H; reflexivity).
 Qed.
 
-Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), H=H -> False.
+Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False.
 Proof.
   intros.
-  autorewrite with base0 in H using try (apply H1; reflexivity).
-Qed.
-
-Lemma ResAck2 : forall H:(Ack 2 2 = 7 -> False), H=H  -> False.
-Proof.
-  intros.
-  autorewrite with base0 in *;
-    apply H1;reflexivity.
+  autorewrite with base0 in *.
+    apply H;reflexivity.
 Qed.