From 80b91aa1e83097efd006cfed5f57e4826a1ab0c8 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 1 Jun 2012 19:53:57 +0000
Subject: Cleaning Pp.ppnl use

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15413 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/xml/cic2acic.ml            | 11 +----------
 plugins/xml/doubleTypeInference.ml |  4 ++--
 plugins/xml/proofTree2Xml.ml4      | 22 +---------------------
 3 files changed, 4 insertions(+), 33 deletions(-)

(limited to 'plugins/xml')

diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index e29fcd0e8..62f7cc7cf 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -351,7 +351,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.pr_lconstr tt)) ; assert false
+Pp.msg_debug (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.      *)
@@ -363,15 +363,6 @@ Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-ty
               (Termops.refresh_universes tt)) ;
            D.expected = None}
         in
-(* Debugging only:
-print_endline "TERMINE:" ; flush stdout ;
-Pp.ppnl (Printer.pr_lconstr tt) ; flush stdout ;
-print_endline "TIPO:" ; 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 ;
-*)
          let innersort =
           let synthesized_innersort =
            get_sort_family_of env evar_map synthesized
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index 24a383250..b1838f4a4 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -147,7 +147,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
 (try
         Typeops.judge_of_type u
  with _ -> (* Successor of a non universe-variable universe anomaly *)
- (Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ;
+  Pp.msg_warning (Pp.str "Universe refresh performed!!!");
   Typeops.judge_of_type (Termops.new_univ ())
 )
 
@@ -239,7 +239,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.pr_lconstr cstr)) ; flush stdout ) ;
+ Pp.msg_warning (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.pr_lconstr cstr));
        Acic.CicHash.add subterms_to_types cstr types ;
        E.make_judge cstr res
 
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index a45b8cda4..033e83410 100644
--- a/plugins/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
@@ -56,16 +56,6 @@ let constr_to_xml obj sigma env =
     Errors.anomaly
      ("Problem during the conversion of constr into XML: " ^
       Printexc.to_string e)
-(* CSC: debugging stuff
-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.pr_lconstr_env rel_env obj') ;
-Pp.ppnl (Pp.str "RAW-TERM:") ;
-Pp.ppnl (Printer.pr_lconstr obj') ;
-Xml.xml_empty "MISSING TERM" [] (*; raise e*)
-*)
 ;;
 
 let first_word s =
@@ -98,20 +88,10 @@ let
  let module X = Xml in
   let ids_of_node node =
    let constr = Proof2aproof.ProofTreeHash.find proof_tree_to_constr node in
-(*
-let constr =
- try
-    Proof2aproof.ProofTreeHash.find proof_tree_to_constr node
- with _ -> Pp.ppnl (Pp.(++) (Pp.str "Node of the proof-tree that generated
-no lambda-term: ") (Refiner.print_script true (Evd.empty)
-(Global.named_context ()) node)) ; assert false (* Closed bug, should not
-happen any more *)
-in
-*)
    try
     Some (Acic.CicHash.find constr_to_ids constr)
    with _ ->
-Pp.ppnl (Pp.(++) (Pp.str
+Pp.msg_warning (Pp.(++) (Pp.str
 "The_generated_term_is_not_a_subterm_of_the_final_lambda_term")
 (Printer.pr_lconstr constr)) ;
     None
-- 
cgit v1.2.3