axiom-

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

diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml
index d2fa70184dc87169ebc5feae4180271faf2fcf3a..95d26c0731a19378481ac9fe62b93b7625df3010 100644 (file)
--- a/matita/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml
@@ -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 =