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

2 files changed, 29 insertions, 36 deletions

diff --git a/dev/include b/dev/include
index bbee6ac742..eabf79a481 100644
--- a/dev/include
+++ b/dev/include
@@ -23,7 +23,6 @@
 #install_printer  (* proof *)  pproof;;
 #install_printer  (* evar_map *)  prevm;;
 #install_printer  (* evar_defs *)  prevd;;
-#install_printer  (* walking_constraints *)  prwc;;
 #install_printer  (* clenv *) prclenv;;
 #install_printer  (* env *) ppenv;;
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 1aac94ffd1..df31c6d9a5 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -19,27 +19,44 @@ open Univ
 open Proof_trees
 open Environ
 open Printer
+open Tactic_printer
 open Refiner
 open Tacmach
 open Term
 open Termops
 open Clenv
 open Cerrors
+open Evd
 
 let _ = Constrextern.print_evar_arguments := true
 
-let pP s = pp (hov 0 s)
-
-let prast c = pp(print_ast c)
+(* name printers *)
+let prid id = pp (pr_id id)
+let prlab l = pp (pr_lab l)
+let prmsid msid = pp (str (debug_string_of_msid msid))
+let prmbid mbid = pp (str (debug_string_of_mbid mbid))
+let prdir dir = pp (pr_dirpath dir)
+let prmp mp = pp(str (string_of_mp mp))
+let prkn kn = pp(pr_kn kn)
+let prsp sp = pp(pr_sp sp)
+let prqualid qid = pp(pr_qualid qid)
 
-let prastpat c = pp(print_astpat c)
-let prastpatl c = pp(print_astlpat c)
-let ppterm x = pp(prterm x)
+(* term printers *)
+let ppterm x = pp(Termops.print_constr x)
 let ppsterm x = ppterm (Declarations.force x)
 let ppterm_univ x = Constrextern.with_universes ppterm x
 let pprawterm = (fun x -> pp(pr_rawterm x))
 let pppattern = (fun x -> pp(pr_pattern x))
 let pptype = (fun x -> pp(prtype x))
+let ppfconstr c = ppterm (Closure.term_of_fconstr c)
+
+
+let pP s = pp (hov 0 s)
+
+let prast c = pp(print_ast c)
+
+let prastpat c = pp(print_astpat c)
+let prastpatl c = pp(print_astlpat c)
 
 let safe_prglobal = function 
   | ConstRef kn -> pp (str "CONSTREF(" ++ pr_kn kn ++ str ")")
@@ -51,21 +68,6 @@ let safe_prglobal = function
 
 let prglobal x = try pp(pr_global x) with _ -> safe_prglobal x
 
-let prid id = pp (pr_id id)
-let prlab l = pp (pr_lab l)
-
-let prmsid msid = pp (str (debug_string_of_msid msid))
-let prmbid mbid = pp (str (debug_string_of_mbid mbid))
-
-let prdir dir = pp (pr_dirpath dir)
-
-let prmp mp = pp(str (string_of_mp mp))
-let prkn kn = pp(pr_kn kn)
-
-let prsp sp = pp(pr_sp sp)
-
-let prqualid qid = pp(pr_qualid qid)
-
 let prconst (sp,j) =
     pp (str"#" ++ pr_kn sp ++ str"=" ++ prterm j.uj_val)
 
@@ -76,24 +78,17 @@ let genprj f j = let (c,t) = f j in (c ++ str " : " ++ t)
 
 let prj j = pp (genprj prjudge j)
 
-let prgoal g = pp(prgl g)
-
-let prsigmagoal g = pp(prgl (sig_it g))
+(* proof printers *)
+let prevm evd = pp(pr_evar_map evd)
+let prevd evd = pp(pr_evar_defs evd)
+let prclenv clenv = pp(pr_clenv clenv)
+let prgoal g = pp(db_pr_goal g)
 
+let prsigmagoal g = pp(pr_goal (sig_it g))
 let prgls gls = pp(pr_gls gls)
-
 let prglls glls = pp(pr_glls glls)
-
 let pproof p = pp(print_proof Evd.empty empty_named_context p)
 
-let prevm evd = pp(pr_decls evd)
-
-let prevd evd = prevm(Evd.evars_of evd)
-
-let prwc wc = pp(pr_evc wc)
-
-let prclenv clenv = pp(pr_clenv clenv)
-
 let print_uni u = (pp (pr_uni u))
 
 let pp_universes u = pp (str"[" ++ pr_universes u ++ str"]")
@@ -300,4 +295,3 @@ let _ =
        | _ -> bad_vernac_args "PrintPureConstr")
 *)
 
-let ppfconstr c = ppterm (Closure.term_of_fconstr c)