diff options
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 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 |