- (* 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
+ let rec aux context' args (resty,subst,metasenv) =
+ function
+ [] -> resty,subst,metasenv
+ | (arg,argty)::tl ->
+ let args' =
+ List.map
+ (function
+ None -> assert false
+ | Some t -> Some (CicMetaSubst.lift subst 1 t)
+ ) args in
+ let argty' = CicMetaSubst.lift subst (List.length args) argty in
+ let context'' = Some (Cic.Anonymous, Cic.Decl argty') :: context' in
+ let (metasenv, idx) =
+ CicMkImplicit.mk_implicit metasenv (context'' @ context) in
+ let irl =
+ (Some (Cic.Rel 1))::args'@(CicMkImplicit.identity_relocation_list_for_metavariable ~start:2 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
+ aux context'' (Some arg :: args)
+ (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
+ in
+ aux [] [] (hetype,subst,metasenv) tlbody_and_type