appel de Zenon

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

1 files changed, 4 insertions, 4 deletions

diff --git a/contrib/dp/test2.v b/contrib/dp/test2.v
index 59f8807f9..8aba348d8 100644
--- a/contrib/dp/test2.v
+++ b/contrib/dp/test2.v
@@ -12,14 +12,15 @@ Definition neg (z:Z) : Z := match z with
   end.
 
 Goal forall z, neg (neg z) = z.
-  zenon.
   Admitted.
 
 Open Scope nat_scope.
 Print plus.
 
 Goal forall x, x+0=x.
-  induction x; zenon.
+  induction x.
+  zenon.
+  zenon.
   (* simplify resoud le premier, pas le second *)
   Admitted.
 
@@ -35,7 +36,7 @@ Fixpoint even (n:nat) : Prop :=
   end.
 
 Goal even 4%nat.
-  zenon.
+  try zenon.
   Admitted.
 
 Definition p (A B:Set) (a:A) (b:B) : list (A*B) := cons (a,b) nil.
@@ -49,7 +50,6 @@ end.
 
 Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1.
 
-zenon.
 Admitted.
 
 (*