(no commit message)

[helm.git] / matitaB / components / ng_disambiguation / nCicDisambiguate.ml

diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml
index ff6f70e946da0ebc17bc78ceff786beef99a0677..c34a5731505c0b9b38d10b11ad91ab1ca9387ce7 100644 (file)
--- a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml
@@ -654,8 +654,8 @@ let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names
                | DisambiguateTypes.Symbol _ -> "SYM"
                | DisambiguateTypes.Num _ -> "NUM"
              in
-             prerr_endline (Printf.sprintf "lookup_choices of %s returns length %d" id
-               (List.length res));
+             debug_print (lazy (Printf.sprintf "lookup_choices of %s returns length %d" id
+               (List.length res)));
              res
           with Not_found -> [])
    in