(* returns an identifier which is fresh in the context *)
(* and that resembles [name] as much as possible. *)
(* [typ] will be the type of the variable *)
-let mk_fresh_name context name ~typ =
+let mk_fresh_name metasenv context name ~typ =
let module C = Cic in
let basename =
match name with
C.Anonymous ->
(*CSC: great space for improvements here *)
(try
- (match CicTypeChecker.type_of_aux' [] context typ with
+ (match CicTypeChecker.type_of_aux' metasenv context typ with
C.Sort C.Prop
| C.Sort C.CProp -> "H"
| C.Sort C.Set -> "x"