X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fcic_unification%2FcicRefine.mli;h=30b264455246890438191bc2a1a0a9757db652fa;hb=396a578b680e7fdb9d262822184e52f0d4d5086b;hp=224a7586c957dfbf91e4704917489a348158b43a;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/cic_unification/cicRefine.mli b/components/cic_unification/cicRefine.mli
index 224a7586c..30b264455 100644
--- a/components/cic_unification/cicRefine.mli
+++ b/components/cic_unification/cicRefine.mli
@@ -46,3 +46,6 @@ val typecheck :
 
 val insert_coercions: bool ref (* initially true *)
 
+val pack_coercion_obj: Cic.obj -> Cic.obj
+
+val pack_coercion_metasenv: Cic.metasenv -> Cic.metasenv