component "substitution" updated to new syntax ...

[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 b9ea25cfa98bcc60422943c6be840bd88c3ede7a..1d3242804a44f280f91ee3c7a50c439b587acae4 100644 (file)
--- a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml
@@ -18,7 +18,7 @@ open DisambiguateTypes
 module Ast = NotationPt
 module NRef = NReference 
 
-let debug_print s = prerr_endline (Lazy.force s);;
+(*let debug_print s = prerr_endline (Lazy.force s);;*)
 let debug_print _ = ();;
 
 let cic_name_of_name = function