(* mk_fresh_name context name typ *)
(* 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 *)
(* mk_fresh_name context name typ *)
(* 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 *)
- prerr_endline "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name" ;
+ debug_print "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name" ;