diff options
Diffstat (limited to 'test-suite')
-rwxr-xr-x | test-suite/check | 4 | ||||
-rw-r--r-- | test-suite/modules/modul.v | 2 | ||||
-rw-r--r-- | test-suite/success/TestRefine.v (renamed from test-suite/tactics/TestRefine.v) | 17 |
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. |