4 files changed, 15 insertions, 8 deletions
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 36e4f0dc9..6d0ad0fb0 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -22,7 +22,12 @@ let debug = ref false
 
 let deb_mess s =
   if !debug then begin
-    msgnl s;  pp_flush()
+    msgnl s; pp_flush()
+  end
+
+let deb_print f x =
+  if !debug then begin
+    msgnl (f x); pp_flush()
   end
 
 let list_of_some = function
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli
index 3dbae5cd0..e93f20a61 100644
--- a/contrib/correctness/pmisc.mli
+++ b/contrib/correctness/pmisc.mli
@@ -72,4 +72,5 @@ val abstract : (identifier * constr) list -> constr -> constr
 
 val debug : bool ref
 val deb_mess : Pp.std_ppcmds -> unit
+val deb_print : ('a -> Pp.std_ppcmds) -> 'a -> unit
 
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 097ddd7da..e78e9fd81 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -43,33 +43,33 @@ let coqast_of_prog p =
   let p = Ptyping.states ren env p in
   let ((_,v),_,_,_) as c = p.info.kappa in
   Perror.check_for_not_mutable p.loc v;
-  deb_mess (pp_type_c c);
+  deb_print pp_type_c c;
 
   (* 3. propagation annotations *)
   let p = Pwp.propagate ren p in
 
   (* 4a. traduction type *)
   let ty = Pmonad.trad_ml_type_c ren env c in
-  deb_mess (Printer.prterm ty);
+  deb_print (Printer.prterm_env (Global.env())) ty;
 
   (* 4b. traduction terme (terme intermédiaire de type cc_term) *)
   deb_mess 
     (fnl () ++ str"Mlize.trad: Translation program -> cc_term..." ++ fnl ());
   let cc = Pmlize.trans ren p in
   let cc = Pred.red cc in
-  deb_mess (Putil.pp_cc_term cc);
+  deb_print Putil.pp_cc_term cc;
 
   (* 5. traduction en constr *)
   deb_mess 
     (fnl () ++ str"Pcic.constr_of_prog: Translation cc_term -> rawconstr..." ++ 
        fnl ());
   let r = Pcic.rawconstr_of_prog cc in
-  deb_mess (Printer.pr_rawterm r);
+  deb_print Printer.pr_rawterm r;
 
   (* 6. résolution implicites *)
   deb_mess (fnl () ++ str"Resolution implicits (? => Meta(n))..." ++ fnl ());
   let oc = understand_gen_tcc Evd.empty (Global.env()) [] [] None r in
-  deb_mess (Printer.prterm (snd oc));
+  deb_print (Printer.prterm_env (Global.env())) (snd oc);
 
   p,oc,ty,v
 
@@ -230,7 +230,7 @@ let correctness s p opttac =
   deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ());
   let oc = reduce_open_constr oc in
   deb_mess (str"AFTER REDUCTION:" ++ fnl ());
-  deb_mess (Printer.prterm (snd oc));
+  deb_mess (Printer.prterm_env (Global.env()) (snd oc));
   let tac = (tclTHEN (Refine.refine_tac oc) automatic) in
   let tac = match opttac with 
     | None -> tac
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index dbb903ab1..5aa497d7f 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -232,7 +232,8 @@ and c_of_constr c =
 
 open Pp
 open Util
-open Printer
+
+let prterm x = Printer.prterm_env (Global.env()) x
 
 let pp_pre = function
     [] -> (mt ())