Imported Upstream version 8.0pl3upstream/8.0pl3

3 files changed, 6 insertions, 17 deletions

diff --git a/test-suite/check b/test-suite/check
index 378c8e5d..fdc7b2d6 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -84,7 +84,8 @@ test_output() {
 	    nbtestsok=`expr $nbtestsok + 1`
         else 
 	    echo "Error! (unexpected output)"
-        fi 
+        fi
+	rm $tmpoutput
     done
 }
 
@@ -106,6 +107,7 @@ test_parser() {
             echo "Ok"
             nbtestsok=`expr $nbtestsok + 1`
         fi
+	rm $tmpoutput
     done
     fi
 }
diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v
index 5612ea75..84942da1 100644
--- a/test-suite/modules/modul.v
+++ b/test-suite/modules/modul.v
@@ -33,7 +33,7 @@ Save.
 Check (O#O).
 Locate rel.
 
-Locate M.
+Locate Library M.
 
 Module N:=Top.M.
 
diff --git a/test-suite/tactics/TestRefine.v b/test-suite/success/TestRefine.v
index f752c5bc..ee3d7e3f 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.