tactics.ml.patch

164a165
> let then_, thenl_ = (THEN), (THENL);;
750c751
< let (pp_print_goal:Format.formatter->goal->unit) =
---
> let (pp_print_goal: formatter->goal->unit) =
757,758c758,759
<     Format.pp_print_string fmt (string_of_int3 n);
<     Format.pp_print_string fmt " [";
---
>     pp_print_string fmt (string_of_int3 n);
>     pp_print_string fmt " [";
762,763c763,764
<     Format.pp_print_string fmt "]";
<     (if not (s = "") then (Format.pp_print_string fmt (" ("^s^")")) else ());
---
>     pp_print_string fmt "]";
>     (if not (s = "") then (pp_print_string fmt (" ("^s^")")) else ());
765c766
<     Format.pp_print_newline fmt () in
---
>     pp_print_newline fmt () in
771,773c772,774
<     Format.pp_print_newline fmt ();
<     if asl <> [] then (print_hyps fmt 0 (rev asl); Format.pp_print_newline fmt ()) else ();
<     pp_print_qterm fmt w; Format.pp_print_newline fmt ();;
---
>     pp_print_newline fmt ();
>     if asl <> [] then (print_hyps fmt 0 (rev asl); pp_print_newline fmt ());
>     pp_print_qterm fmt w; pp_print_newline fmt ();;
775c776
< let (pp_print_goalstack:Format.formatter->goalstack->unit) =
---
> let (pp_print_goalstack: formatter->goalstack->unit) =
782c783
<     Format.pp_print_string fmt s; Format.pp_print_newline fmt ();
---
>     pp_print_string fmt s; pp_print_newline fmt ();
786c787
<     if l = [] then Format.pp_print_string fmt "Empty goalstack"
---
>     if l = [] then pp_print_string fmt "Empty goalstack"
797,798c798,799
< let print_goal = pp_print_goal Format.std_formatter;;
< let print_goalstack = pp_print_goalstack Format.std_formatter;;
---
> let print_goal = Pretty.print_stdout pp_print_goal;;
> let print_goalstack = Pretty.print_stdout pp_print_goalstack;;
861,863c862,863
<   let asl,t' = dest_thm th in
<   if asl <> [] then failwith "prove: additional assumptions in result"
<   else if t' = t then th else
---
>   let t' = concl th in
>   if t' = t then th else
873c873
< let (refine:refinement->goalstack) =
---
> let (refine:refinement->unit) =
880c880
<     !current_goalstack;;
---
>     print_goalstack (!current_goalstack);;
893c893
<   !current_goalstack;;
---
>   print_goalstack (!current_goalstack);;
896c896
<   let fvs = sort (<) (map (fst o dest_var) (frees t)) in
---
>   let fvs = sort String.(<) (map (fst o dest_var) (frees t)) in
907c907
<   !current_goalstack;;
---
>   print_goalstack (!current_goalstack);;
910c910
<   !current_goalstack;;
---
>   print_goalstack (!current_goalstack);;
928,929c928,933
< #install_printer pp_print_goal;;
< #install_printer pp_print_goalstack;;
---
> let pp_goal =
>   Pretty_printer.token o Pretty.print_to_string pp_print_goal;;
> 
> let pp_goalstack =
>   Pretty_printer.token o Pretty.print_to_string pp_print_goalstack;;
>