3 files changed, 5 insertions, 5 deletions
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index e79d14249d..81e175232f 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -280,12 +280,12 @@ let print_check judg =
  let value_ct_ast = 
      (try translate_constr false (Global.env()) value 
       with UserError(f,str) ->
-           raise(UserError(f,Printer.prterm value ++
+           raise(UserError(f,Printer.pr_lconstr value ++
 			      fnl () ++ str ))) in
  let type_ct_ast =
      (try translate_constr false (Global.env()) typ
       with UserError(f,str) ->
-           raise(UserError(f, Printer.prterm value ++ fnl() ++ str))) in
+           raise(UserError(f, Printer.pr_lconstr value ++ fnl() ++ str))) in
  ((ctf_SearchResults !global_request_id),
  (Some  (P_pl
   (CT_premises_list
@@ -557,7 +557,7 @@ let rec hyp_pattern_filter pat name a c =
     match kind_of_term c with
       | Prod(_, hyp, c2) -> 
 	  (try
-(*	     let _ = msgnl ((str "WHOLE ") ++ (Printer.prterm c)) in
+(*	     let _ = msgnl ((str "WHOLE ") ++ (Printer.pr_lconstr c)) in
              let _ = msgnl ((str "PAT ") ++ (Printer.pr_pattern pat)) in *)
              if Matching.is_matching pat hyp then
 	       (msgnl (str "ok"); true)
diff --git a/contrib/interface/showproof_ct.ml b/contrib/interface/showproof_ct.ml
index f6ab47376b..07ac73b6aa 100644
--- a/contrib/interface/showproof_ct.ml
+++ b/contrib/interface/showproof_ct.ml
@@ -130,7 +130,7 @@ let rec sp_print x =
 	     | "\n" -> fnl ()
 	     | "Retour chariot pour Show proof" -> fnl ()
 	     |_ -> str s)
-     | CT_text_formula  f -> prterm (Hashtbl.find ct_FORMULA_constr f)
+     | CT_text_formula  f -> pr_lconstr (Hashtbl.find ct_FORMULA_constr f)
      | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "to_prove");
 		   CT_text_path (CT_signed_int_list p);
 		   CT_coerce_ID_to_TEXT (CT_ident "goal");
diff --git a/contrib/interface/translate.mli b/contrib/interface/translate.mli
index 65d8331b2d..9f25ce38a4 100644
--- a/contrib/interface/translate.mli
+++ b/contrib/interface/translate.mli
@@ -6,6 +6,6 @@ open Term;;
 
 val translate_goal : goal -> ct_RULE;;
 (* The boolean argument indicates whether names from the environment should *)
-(*  be avoided (same interpretation as for prterm_env and ast_of_constr)    *)
+(*  be avoided (same interpretation as for pr_lconstr_env and ast_of_constr)    *)
 val translate_constr : bool -> env -> constr -> ct_FORMULA;;
 val translate_path : int list -> ct_SIGNED_INT_LIST;;