diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-17 20:28:19 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-17 20:28:19 +0000 |
| commit | ed29c6bbe9a45e7d3996c230a6cc2bf7b11848f1 (patch) | |
| tree | f898c771227a1e111be1bac0431d42d04b0166f6 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2b2dc3138..e8c8516bf 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -23,6 +23,7 @@ open Proof_trees open Constrintern open Prettyp open Printer +open Tactic_printer open Tacinterp open Command open Goptions @@ -79,20 +80,20 @@ let show_node () = let pf = proof_of_pftreestate pts and cursor = cursor_of_pftreestate pts in msgnl (prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++ - prgl (goal_of_proof pf) ++ fnl () ++ + pr_goal (goal_of_proof pf) ++ fnl () ++ (match pf.Proof_type.ref with | None -> (str"BY <rule>") | Some(r,spfl) -> - (str"BY " ++ Refiner.pr_rule r ++ fnl () ++ + (str"BY " ++ pr_rule r ++ fnl () ++ str" " ++ - hov 0 (prlist_with_sep pr_fnl prgl + hov 0 (prlist_with_sep pr_fnl pr_goal (List.map goal_of_proof spfl))))) let show_script () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and evc = evc_of_pftreestate pts in - msgnl (Refiner.print_treescript true evc (Global.named_context()) pf) + msgnl (print_treescript true evc (Global.named_context()) pf) let show_top_evars () = let pfts = get_pftreestate () in @@ -104,7 +105,7 @@ let show_prooftree () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and evc = evc_of_pftreestate pts in - msg (Refiner.print_proof evc (Global.named_context()) pf) + msg (print_proof evc (Global.named_context()) pf) let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) () @@ -1006,10 +1007,10 @@ let apply_subproof f occ = f evc (Global.named_context()) pf let explain_proof occ = - msg (apply_subproof (Refiner.print_treescript true) occ) + msg (apply_subproof (print_treescript true) occ) let explain_tree occ = - msg (apply_subproof Refiner.print_proof occ) + msg (apply_subproof print_proof occ) let vernac_show = function | ShowGoal nopt -> |