diff options
| author | ppedrot | 2012-06-01 19:53:57 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-01 19:53:57 +0000 |
| commit | 80b91aa1e83097efd006cfed5f57e4826a1ab0c8 (patch) | |
| tree | 75f2746f738c2b2c111b701f80d59d10f80c75f7 /plugins/xml/cic2acic.ml | |
| parent | cf7660a3a8932ee593a376e8ec7ec251896a72e3 (diff) | |
Cleaning Pp.ppnl use
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15413 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml/cic2acic.ml')
| -rw-r--r-- | plugins/xml/cic2acic.ml | 11 |
1 files changed, 1 insertions, 10 deletions
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 |