2 files changed, 11 insertions, 11 deletions
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index bd742b9dfc..5994fb38d4 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -51,7 +51,7 @@ let coqast_of_prog p =
 
   (* 4a. traduction type *)
   let ty = Pmonad.trad_ml_type_c ren env c in
-  deb_print (Printer.prterm_env (Global.env())) ty;
+  deb_print (Printer.pr_lconstr_env (Global.env())) ty;
 
   (* 4b. traduction terme (terme intermédiaire de type cc_term) *)
   deb_mess 
@@ -65,12 +65,12 @@ let coqast_of_prog p =
     (fnl () ++ str"Pcic.constr_of_prog: Translation cc_term -> rawconstr..." ++ 
        fnl ());
   let r = Pcic.rawconstr_of_prog cc in
-  deb_print Printer.pr_rawterm r;
+  deb_print Printer.pr_lrawconstr 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_print (Printer.prterm_env (Global.env())) (snd oc);
+  deb_print (Printer.pr_lconstr_env (Global.env())) (snd oc);
 
   p,oc,ty,v
 
@@ -248,7 +248,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_print (Printer.prterm_env (Global.env())) (snd oc);
+  deb_print (Printer.pr_lconstr_env (Global.env())) (snd oc);
   let tac = (tclTHEN (Extratactics.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 45fdb75ec7..29064578f1 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -231,26 +231,26 @@ and c_of_constr c =
 open Pp
 open Util
 
-let prterm x = Printer.prterm_env (Global.env()) x
+let pr_lconstr x = Printer.pr_lconstr_env (Global.env()) x
 
 let pp_pre = function
     [] -> (mt ())
   | l  ->
       hov 0 (str"pre " ++ 
 	       prlist_with_sep (fun () -> (spc ())) 
-		 (fun x -> prterm x.p_value) l)
+		 (fun x -> pr_lconstr x.p_value) l)
 
 let pp_post = function
     None -> (mt ())
-  | Some c -> hov 0 (str"post " ++ prterm c.a_value)
+  | Some c -> hov 0 (str"post " ++ pr_lconstr c.a_value)
 
 let rec pp_type_v = function
     Ref v -> hov 0 (pp_type_v v ++ spc () ++ str"ref")
-  | Array (cc,v) -> hov 0 (str"array " ++ prterm cc ++ str" of " ++ pp_type_v v)
+  | Array (cc,v) -> hov 0 (str"array " ++ pr_lconstr cc ++ str" of " ++ pp_type_v v)
   | Arrow (b,c) -> 
       hov 0 (prlist_with_sep (fun () -> (mt ())) pp_binder b ++ 
 	       pp_type_c c)
-  | TypePure c -> prterm c
+  | TypePure c -> pr_lconstr c
 
 and pp_type_c ((id,v),e,p,q) =
   hov 0 (str"returns " ++ pr_id id ++ str":" ++ pp_type_v v ++ spc () ++ 
@@ -297,7 +297,7 @@ let rec pp_cc_term = function
   | CC_case _ ->
       hov 0 (str"<Case: not yet implemented>")
   | CC_expr c ->
-      hov 0 (prterm c)
+      hov 0 (pr_lconstr c)
   | CC_hole c ->
-      (str"(?::" ++ prterm c ++ str")")
+      (str"(?::" ++ pr_lconstr c ++ str")")