From: Claudio Sacerdoti Coen Date: Tue, 6 Feb 2007 18:47:05 +0000 (+0000) Subject: Bug fixed in the computation of the disambiguation domain of a let...rec. X-Git-Tag: make_still_working~6486 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a4f2e0626c1141b58a58ca3956154462eb234d89;p=helm.git Bug fixed in the computation of the disambiguation domain of a let...rec. --- diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 5c198cb59..ac26903b1 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -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