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: 0.4.95@7852~627 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4f12355502a0af2edfa98023270c21a9f0d83533;p=helm.git Bug fixed in the computation of the disambiguation domain of a let...rec. --- diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml index 5c198cb59..ac26903b1 100644 --- a/components/cic_disambiguation/disambiguate.ml +++ b/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