diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/first-order/ground.ml | 2 | ||||
| -rwxr-xr-x | contrib/interface/blast.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/centaur.ml4 | 4 | ||||
| -rw-r--r-- | contrib/interface/debug_tac.ml4 | 4 | ||||
| -rw-r--r-- | contrib/xml/proof2aproof.ml | 2 |
5 files changed, 7 insertions, 7 deletions
diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml index 690fc48c5..bd155fd51 100644 --- a/contrib/first-order/ground.ml +++ b/contrib/first-order/ground.ml @@ -61,7 +61,7 @@ let ground_tac solver startseq gl= update_flags (); let rec toptac skipped seq gl= if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 - then Pp.msgnl (Proof_trees.pr_goal (sig_it gl)); + then Pp.msgnl (Printer.pr_goal (sig_it gl)); tclORELSE (axiom_tac seq.gl seq) begin try diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 96dd51ab8..72875cc9b 100755 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -112,7 +112,7 @@ let rec print_info_script sigma osign pf = match pf.ref with | None -> (mt ()) | Some(r,spfl) -> - pr_rule r ++ + Tactic_printer.pr_rule r ++ match spfl with | [] -> (str " " ++ fnl()) diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index 7bf12f3b6..3cc539063 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -362,7 +362,7 @@ let debug_tac2_pcoq tac = try let result = report_error tac the_goal the_ast the_path [] g in (errorlabstrm "DEBUG TACTIC" - (str "no error here " ++ fnl () ++ pr_goal (sig_it g) ++ + (str "no error here " ++ fnl () ++ Printer.pr_goal (sig_it g) ++ fnl () ++ str "the tactic is" ++ fnl () ++ Pptactic.pr_glob_tactic tac); result) @@ -616,7 +616,7 @@ let pcoq_show_goal = function | Some n -> show_nth n | None -> if !pcoq_started = Some true (* = debug *) then - msg (Pfedit.pr_open_subgoals ()) + msg (Printer.pr_open_subgoals ()) else errorlabstrm "show_goal" (str "Show must be followed by an integer in Centaur mode");; diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4 index bf596b284..939c67917 100644 --- a/contrib/interface/debug_tac.ml4 +++ b/contrib/interface/debug_tac.ml4 @@ -554,8 +554,8 @@ let descr_first_error tac = (msgnl (str "Execution of this tactic raised message " ++ fnl () ++ fnl () ++ Cerrors.explain_exn e ++ fnl () ++ fnl () ++ str "on goal" ++ fnl () ++ - pr_goal (sig_it (strip_some !the_goal)) ++ fnl () ++ - str "faulty tactic is" ++ fnl () ++ fnl () ++ + Printer.pr_goal (sig_it (strip_some !the_goal)) ++ + fnl () ++ str "faulty tactic is" ++ fnl () ++ fnl () ++ pr_glob_tactic ((*flatten_then*) !the_ast) ++ fnl ()); tclIDTAC g)) diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml index 5c5ac5d61..9220e8a4d 100644 --- a/contrib/xml/proof2aproof.ml +++ b/contrib/xml/proof2aproof.ml @@ -154,7 +154,7 @@ let extract_open_proof sigma pf = (*CSC: debugging stuff to be removed *) if ProofTreeHash.mem proof_tree_to_constr node then Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ") - (Refiner.print_proof (Evd.evars_of !evd) [] node)) ; + (Tactic_printer.print_proof (Evd.evars_of !evd) [] node)) ; ProofTreeHash.add proof_tree_to_constr node unsharedconstr ; unshared_constrs := S.add unsharedconstr !unshared_constrs ; unsharedconstr |