]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_disambiguation/nCicDisambiguate.ml
Known bug fixed: the rhs of a match over a small singleton inductive type
[helm.git] / matita / components / ng_disambiguation / nCicDisambiguate.ml
index d2fa70184dc87169ebc5feae4180271faf2fcf3a..8e3f267775535c4bba5ae5216ba3af11cd1d77bf 100644 (file)
@@ -18,8 +18,8 @@ open DisambiguateTypes
 module Ast = NotationPt
 module NRef = NReference 
 
-let debug_print s = prerr_endline (Lazy.force s);;
-let debug_print _ = ();;
+let debug = ref false;;
+let debug_print s = if !debug then prerr_endline (Lazy.force s);;
 
 let cic_name_of_name = function
   | Ast.Ident (n, None) ->  n
@@ -66,6 +66,7 @@ let refine_term (status: #NCicCoercion.status) metasenv subst context uri ~use_c
 let refine_obj status metasenv subst _context _uri ~use_coercions obj _ _ugraph
  ~localization_tbl 
 =
+  (*prerr_endline ((sprintf "TEST_INTERPRETATION: %s" (status#ppobj obj)));*)
   assert (metasenv=[]);
   assert (subst=[]);
   let localise t =