From 80b91aa1e83097efd006cfed5f57e4826a1ab0c8 Mon Sep 17 00:00:00 2001
From: ppedrot
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 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

(limited to 'plugins/xml/cic2acic.ml')

diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index e29fcd0e8f..62f7cc7cf5 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
-- 
cgit v1.2.3