X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=41c24c9ae5a11065df8c8ccc9e5c632911c60cac;hb=a3ff8f4f61a45e8c269322275956fad0805da8bc;hp=ad8028d165a73f4ba5e6923a27cc8daf8cc6e8f1;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;p=helm.git diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index ad8028d16..41c24c9ae 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -380,6 +380,8 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ if localize then match body with CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) -> + (* since we avoid the letin, the context has no + * recfuns in it *) let l' = List.map (aux ~localize loc context) l in `AvoidLetIn (n,l') | _ -> assert false @@ -785,6 +787,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