]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/disambiguation/multiPassDisambiguator.ml
1) Bug fixed: the case Meta(i) vs Meta(i) was handled in a particular way,
[helm.git] / helm / software / components / disambiguation / multiPassDisambiguator.ml
index 86d037742652c99085ff07092dceaf371447d5dd..5767aa3e3f04f09564beb9aa1d70d64f846f9335 100644 (file)
@@ -27,9 +27,9 @@
 
 open Printf
 
-let debug = false;;
+let debug = ref false;;
 let debug_print s =
- if debug then prerr_endline (Lazy.force s);;
+ if !debug then prerr_endline (Lazy.force s) else ();;
 
 exception DisambiguationError of
  int *