added default for matita.noiinertypes

[helm.git] / components / library / refinementTool.ml

diff --git a/components/library/refinementTool.ml b/components/library/refinementTool.ml
index 70af8740b2294b498ddcc9c9e0b524f98023d0ec..b78246987b8f6c54ecb32608906267b11264558e 100644 (file)
--- a/components/library/refinementTool.ml
+++ b/components/library/refinementTool.ml
@@ -30,12 +30,12 @@ type type_of_rc =
   (* 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;
 }