X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=1a318362500e115107a1312cdf46bcd0294aeb30;hb=3f676ab6acafa32514a44bc84d287f44dbc5389e;hp=5c198cb5962bf06bef7850892ba384ffe2c35618;hpb=8402a4a856b031916b1e2b1354b863933763fa58;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 5c198cb59..1a3183625 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -86,7 +86,7 @@ let uniq_domain dom =
  in
   snd (aux [] dom)
 
-let debug = true
+let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (*
@@ -684,7 +684,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
                   CicNotationUtil.cic_name_of_name var :: context,
                   domain_of_term_option ~loc ~context ty @ res)
                 (add_defs context,[]) params))
-            @ domain_of_term_option ~loc ~context typ
+            @ domain_of_term_option ~loc ~context:context' typ
             @ domain_of_term ~loc ~context:context' body
           ) [] defs
       in