- and eat_prods subst metasenv context hetype =
- function
- [] -> hetype,subst,metasenv
- | (hete, hety)::tl ->
- (match (CicMetaSubst.whd metasenv subst context hetype) with
- Cic.Prod (n,s,t) ->
- let subst',metasenv' =
- CicUnification.fo_unif_subst subst context metasenv s hety
- in
- CicReduction.fdebug := -1 ;
- eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
- | Cic.Meta _ as t ->
- raise
- (Uncertain
- ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
- | _ -> raise (NotRefinable "Appl: wrong Prod-type")
- )
+ and eat_prods subst metasenv context hetype tlbody_and_type =
+ (* TODO to be reviewed *)
+ List.fold_left
+ (fun (resty, subst, metasenv) (arg, argty) ->
+ let context' = Some (Cic.Anonymous, Cic.Decl argty) :: context in
+ let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv context' in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context'
+ in
+ let newmeta = Cic.Meta (idx, irl) in
+ let prod = Cic.Prod (Cic.Anonymous, argty, newmeta) in
+ let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
+ let (subst, metasenv) =
+ CicUnification.fo_unif_subst subst context metasenv resty prod
+ in
+ (CicMetaSubst.subst subst arg newmeta, subst, metasenv))
+ (hetype, subst, metasenv) tlbody_and_type
+