)
;;
-let mk_fresh_name_callback context name ~typ =
+let mk_fresh_name_callback metasenv context name ~typ =
let fresh_name =
- match FreshNamesGenerator.mk_fresh_name context name ~typ with
+ match FreshNamesGenerator.mk_fresh_name metasenv context name ~typ with
Cic.Name fresh_name -> fresh_name
| Cic.Anonymous -> assert false
in