diff options
| author | barras | 2004-09-17 20:28:19 +0000 |
|---|---|---|
| committer | barras | 2004-09-17 20:28:19 +0000 |
| commit | ed29c6bbe9a45e7d3996c230a6cc2bf7b11848f1 (patch) | |
| tree | f898c771227a1e111be1bac0431d42d04b0166f6 /contrib/interface | |
| parent | 59c2fa12e257ae6087e0580e0d7abca3552421b8 (diff) | |
restructuration des printers: proofs passe avant parsing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -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 |
3 files changed, 5 insertions, 5 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 96dd51ab8b..72875cc9b8 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 7bf12f3b6f..3cc5390639 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 bf596b2842..939c67917d 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)) |