- FreshNamesGenerator.mk_fresh_name
- (CicMetaSubst.apply_subst_metasenv subst metasenv)
- (CicMetaSubst.apply_subst_context subst context)
- Cic.Anonymous
- (CicMetaSubst.apply_subst subst argty) in
+ (* The name must be fresh for (context'@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 =
+ FreshNamesGenerator.mk_fresh_name
+ (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'@context) name_hint (Cic.Sort Cic.Prop)
+ in