X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FrefinementTool.ml;h=b78246987b8f6c54ecb32608906267b11264558e;hb=82f61808091c59aa884eb232b96ee1c655dcb39a;hp=e9dae40d945cd62413c08a257530c568d621944f;hpb=7e30c63fcf9f9fe1780ba7aa4d95fd0d8658548b;p=helm.git

diff --git a/helm/software/components/library/refinementTool.ml b/helm/software/components/library/refinementTool.ml
index e9dae40d9..b78246987 100644
--- a/helm/software/components/library/refinementTool.ml
+++ b/helm/software/components/library/refinementTool.ml
@@ -30,7 +30,7 @@ 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;