X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fcic_unification%2FcicRefine.mli;h=30b264455246890438191bc2a1a0a9757db652fa;hb=590854ef49fa6c6ce12a4e3cd2b480266b62f589;hp=be1069e716ef35459836f464921e77b9315fee05;hpb=3f00ce2e2e2f2d443e942d86c394200554ba2496;p=helm.git

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