From 8568952f9d2f97524d1a150743fc91ca9d0c0d05 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 9 May 2008 11:40:29 +0000 Subject: [PATCH] Bug fixed: the domain of a LetRec was only made by the last function in the mutual block. --- helm/software/components/cic_disambiguation/disambiguate.ml | 1 + 1 file changed, 1 insertion(+) 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 -- 2.39.2