+ let rec mk_prod metasenv context =
+ function
+ [] ->
+ let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ metasenv,Cic.Meta (idx, irl)
+ | (_,argty)::tl ->
+ let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ let meta = Cic.Meta (idx,irl) in
+ let name =
+ (* The name must be fresh for context. *)
+ (* Nevertheless, argty is well-typed only in context. *)
+ (* Thus I generate a name (name_hint) in context and *)
+ (* then I generate a name --- using the hint name_hint *)
+ (* --- that is fresh in (context'@context). *)
+ let name_hint =
+ (* Cic.Name "pippo" *)
+ FreshNamesGenerator.mk_fresh_name metasenv
+(* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
+ (CicMetaSubst.apply_subst_context subst context)
+ Cic.Anonymous
+ (CicMetaSubst.apply_subst subst argty)
+ in
+ (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
+ FreshNamesGenerator.mk_fresh_name
+ [] context name_hint (Cic.Sort Cic.Prop)
+ in
+ let metasenv,target =
+ mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
+ in
+ metasenv,Cic.Prod (name,meta,target)
+ in
+ let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
+ let (subst, metasenv) =
+ fo_unif_subst subst context metasenv hetype hetype'
+ in
+ let rec eat_prods metasenv subst context hetype =
+ function
+ [] -> metasenv,subst,hetype
+ | (hete, hety)::tl ->
+ (match hetype with
+ Cic.Prod (n,s,t) ->
+ let subst,metasenv =
+ fo_unif_subst subst context metasenv hety s
+(*
+ try
+ fo_unif_subst subst context metasenv hety s
+ with _ ->
+ prerr_endline("senza subst fallisce");
+ let hety = CicMetaSubst.apply_subst subst hety in
+ let s = CicMetaSubst.apply_subst subst s in
+ prerr_endline ("unifico = " ^(CicPp.ppterm hety));
+ prerr_endline ("con = " ^(CicPp.ppterm s));
+ fo_unif_subst subst context metasenv hety s *)
+ in
+ (* DEBUG
+ let t1 = CicMetaSubst.subst subst hete t in
+ let t2 = CicSubstitution.subst hete t in
+ prerr_endline ("con subst = " ^(CicPp.ppterm t1));
+ prerr_endline ("senza subst = " ^(CicPp.ppterm t2));
+ prerr_endline("++++++++++metasenv prima di eat_prods:\n" ^
+ (CicMetaSubst.ppmetasenv metasenv subst));
+ prerr_endline("++++++++++subst prima di eat_prods:\n" ^
+ (CicMetaSubst.ppsubst subst));
+ *)
+ eat_prods metasenv subst context
+ (* (CicMetaSubst.subst subst hete t) tl *)
+ (CicSubstitution.subst hete t) tl
+ | _ -> assert false
+ )
+ in
+ let metasenv,subst,t =
+ eat_prods metasenv subst context hetype' tlbody_and_type
+ in
+ t,subst,metasenv
+(*