X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_disambiguation%2Fdisambiguate.ml;h=1a318362500e115107a1312cdf46bcd0294aeb30;hb=14c956f9be9e525fc2dd140e8a2ea6c063c48930;hp=5c198cb5962bf06bef7850892ba384ffe2c35618;hpb=e134b6f156268364d3027e73910c19e9c7e09838;p=helm.git diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml index 5c198cb59..1a3183625 100644 --- a/components/cic_disambiguation/disambiguate.ml +++ b/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