(* these are the same functions of cic_unification/ (eventually wrapped) *)
type kit = {
type_of_aux':
- ?localization_tbl:Token.flocation Cic.CicHash.t ->
+ ?localization_tbl:Stdpp.location Cic.CicHash.t ->
Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph ->
type_of_rc;
pack_coercion_obj: Cic.obj -> Cic.obj;
apply_subst: Cic.substitution -> Cic.term -> Cic.term ;
- ppsubst: Cic.substitution -> string;
+ ppsubst: metasenv:Cic.metasenv -> Cic.substitution -> string;
ppmetasenv: Cic.substitution -> Cic.metasenv -> string;
}