removed debug prerr_endline

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index bd7b334401f68f4e4dbf8139e156697a9bc42c49..4f8f8e78a43a1c9bd34028fc3b5f5b6efe363377 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -250,7 +250,7 @@ let interpretate ~context ~env ast =
                 Cic.MutConstruct (uri, i, j, mk_subst uris)
             | Cic.Meta _ | Cic.Implicit _ as t ->
 (*
-                prerr_endline (sprintf
+                debug_print (sprintf
                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
                   (CicPp.ppterm t)
                   (String.concat "; "
@@ -460,8 +460,8 @@ module Make (C: Callbacks) =
              try
                CicUtil.term_of_uri uri
              with exn ->
-               prerr_endline uri;
-               prerr_endline (Printexc.to_string exn);
+               debug_print uri;
+               debug_print (Printexc.to_string exn);
                assert false
             in
            fun _ _ _ -> term))
@@ -514,7 +514,7 @@ module Make (C: Callbacks) =
               (fun dom_item ->
                 try
                   let len = List.length (lookup_choices dom_item) in
-                  prerr_endline (sprintf "BENCHMARK %s: %d"
+                  debug_print (sprintf "BENCHMARK %s: %d"
                     (string_of_domain_item dom_item) len);
                   len
                 with No_choices _ -> 0)
@@ -615,7 +615,7 @@ module Make (C: Callbacks) =
 (*
         (if benchmark then
           let res_size = List.length res in
-          prerr_endline (sprintf
+          debug_print (sprintf
             ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
             "BENCHMARK:   estimated %.2f")
             !actual_refinements !max_refinements !domain_size res_size