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 ad8028d165a73f4ba5e6923a27cc8daf8cc6e8f1..4b17bef5dfa95eac5c2aabf11f643196c09f9d07 100644 (file)
--- 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