From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 9 May 2008 11:40:29 +0000 (+0000)
Subject: Bug fixed: the domain of a LetRec was only made by the last function in the
X-Git-Tag: make_still_working~5244
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8568952f9d2f97524d1a150743fc91ca9d0c0d05;p=helm.git

Bug fixed: the domain of a LetRec was only made by the last function in the
mutual block.
---

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index ad8028d16..4b17bef5d 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -785,6 +785,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))
+            @ dom
             @ domain_of_term_option ~loc ~context:context' typ
             @ domain_of_term ~loc ~context:context' body
           ) [] defs