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

3 files changed, 9 insertions, 9 deletions

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 =