(* and that resembles [name] as much as possible. *)
(* [typ] will be the type of the variable *)
val mk_fresh_name :
- Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+ subst:Cic.substitution ->
+ Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
(* clean_dummy_dependent_types term *)
(* returns a copy of [term] where every dummy dependent product *)