Commit df68b894 authored by Heiko Becker's avatar Heiko Becker

Fix bug in script output and hol tactics typing

parent a495714e
......@@ -3,7 +3,7 @@ First some tactics that can only work on goals
*)
let intros t = INTRO_TAC t;;
let (split:xtactic) =
let split =
fun g ->
try (CONJ_TAC g) with
|Failure _ -> EQ_TAC g;;
......
......@@ -46,6 +46,6 @@ for file in "${arrHOL[@]}"
do
echo $file
echo ""
time ((ocaml < $file) &>../output/log_$file)
time ((ocaml < $file) &>.$file)
done
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment