X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Flibrary%2FrefinementTool.ml;h=e9dae40d945cd62413c08a257530c568d621944f;hb=84d34c4d0b0a3c923a62cb686966ef66bccb54c8;hp=70af8740b2294b498ddcc9c9e0b524f98023d0ec;hpb=9393a9f9370014c904244358abe4ec6e11a9d158;p=helm.git

diff --git a/components/library/refinementTool.ml b/components/library/refinementTool.ml
index 70af8740b..e9dae40d9 100644
--- a/components/library/refinementTool.ml
+++ b/components/library/refinementTool.ml
@@ -35,7 +35,7 @@ type kit = {
       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;
 }