From dcaefd4a668617504aaf335ed346598b03a80ba1 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
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
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'contrib/xml')

diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index caac70310..bac7ad7c6 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -388,7 +388,7 @@ try
           Acic.CicHash.find terms_to_types tt
 with _ ->
 (*CSC: Warning: it really happens, for example in Ring_theory!!! *)
-Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.prterm tt)) ; assert false
+Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false
          else
           (* We are already in an inner-type and Coscoy's double *)
           (* type inference algorithm has not been applied.      *)
@@ -402,9 +402,9 @@ Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-ty
         in
 (* Debugging only:
 print_endline "TERMINE:" ; flush stdout ;
-Pp.ppnl (Printer.prterm tt) ; flush stdout ;
+Pp.ppnl (Printer.pr_lconstr tt) ; flush stdout ;
 print_endline "TIPO:" ; flush stdout ;
-Pp.ppnl (Printer.prterm synthesized) ; flush stdout ;
+Pp.ppnl (Printer.pr_lconstr synthesized) ; flush stdout ;
 print_endline "ENVIRONMENT:" ; flush stdout ;
 Pp.ppnl (Printer.pr_context_of env) ; flush stdout ;
 print_endline "FINE_ENVIRONMENT" ; flush stdout ;
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index 24676f186..518f6c115 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
 
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index 1de6a4325..578c1ed2f 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -67,9 +67,9 @@ Pp.ppnl (Pp.str "Problem during the conversion of constr into XML") ;
 Pp.ppnl (Pp.str "ENVIRONMENT:") ;
 Pp.ppnl (Printer.pr_context_of rel_env) ;
 Pp.ppnl (Pp.str "TERM:") ;
-Pp.ppnl (Printer.prterm_env rel_env obj') ;
+Pp.ppnl (Printer.pr_lconstr_env rel_env obj') ;
 Pp.ppnl (Pp.str "RAW-TERM:") ;
-Pp.ppnl (Printer.prterm obj') ;
+Pp.ppnl (Printer.pr_lconstr obj') ;
 Xml.xml_empty "MISSING TERM" [] (*; raise e*)
 *)
 ;;
@@ -120,7 +120,7 @@ in
    with _ ->
 Pp.ppnl (Pp.(++) (Pp.str
 "The_generated_term_is_not_a_subterm_of_the_final_lambda_term")
-(Printer.prterm constr)) ;
+(Printer.pr_lconstr constr)) ;
     None
   in
   let rec aux node old_hyps =
-- 
cgit v1.2.3