Activation du test de Refine en v7 pour mémoire avant passage à la v8

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

1 files changed, 2 insertions, 15 deletions

diff --git a/test-suite/tactics/TestRefine.v b/test-suite/success/TestRefine.v
index f752c5bc6f..ee3d7e3f81 100644
--- a/test-suite/tactics/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -182,22 +182,9 @@ Refine (well_founded_induction
       	       	       	       	       	       (fib (pred (pred x0)) ?))
 		     end
 	 end).
-(*********
-Refine (well_founded_induction
-       nat
-       lt ?
-       [_:nat]nat
-       [x0:nat][fib:(x:nat)(lt x x0)->nat]
-         Cases x0 of 
-      	   O     => (S O)
-      	 | (S O) => (S O)
-      	 | (S (S p)) => (plus (fib (pred x0) ?)
-      	       	       	      (fib (pred (pred x0)) ?))
-	 end).
-***********)
 Exact lt_wf.
-Auto.
-Apply lt_trans with m:=(pred x0); Auto.
+Auto with arith.
+Apply lt_trans with m:=(pred x0); Auto with arith.
 Save.