From dcaefd4a668617504aaf335ed346598b03a80ba1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Jan 2006 09:47:32 +0000
Subject: Restructuration et simplification des fonctions d'affichage, de
 détypage et d'"externalisation"; standardisation du nom des fonctions
 d'affichage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/xml/doubleTypeInference.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'contrib/xml/doubleTypeInference.ml')

diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index 24676f1866..518f6c115f 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -40,13 +40,13 @@ let whd_betadeltaiotacprop env evar_map ty =
 Conv_oracle.set_opaque_const cprop;
 prerr_endline "###whd_betadeltaiotacprop:" ;
 let xxx =
-(*Pp.msgerr (Printer.prterm_env env ty);*)
+(*Pp.msgerr (Printer.pr_lconstr_env env ty);*)
 prerr_endline "";
    (fst (Redexpr.reduction_of_red_expr red_exp)) env evar_map ty
 in
 prerr_endline "###FINE" ;
 (*
-Pp.msgerr (Printer.prterm_env env xxx);
+Pp.msgerr (Printer.pr_lconstr_env env xxx);
 *)
 prerr_endline "";
 Conv_oracle.set_transparent_const cprop;
@@ -258,7 +258,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
       in
 (*CSC: debugging stuff to be removed *)
 if Acic.CicHash.mem subterms_to_types cstr then
- (Pp.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.prterm cstr)) ; flush stdout ) ;
+ (Pp.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.pr_lconstr cstr)) ; flush stdout ) ;
        Acic.CicHash.add subterms_to_types cstr types ;
        E.make_judge cstr res
 
-- 
cgit v1.2.3