X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=95d26c0731a19378481ac9fe62b93b7625df3010;hb=f79ad341c99ebaf1a848beac52318db2a82f89f3;hp=d2fa70184dc87169ebc5feae4180271faf2fcf3a;hpb=f4665bcba9c87ecced8746f08da717c767b1a839;p=helm.git diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml index d2fa70184..95d26c073 100644 --- 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 =