X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.mli;h=c3ab49e0abd84dd19a79de242dffb25999928e79;hb=54b20096e701de9f3fb8e10fe2106ab2f6e0d2bf;hp=224a7586c957dfbf91e4704917489a348158b43a;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.mli b/helm/software/components/cic_unification/cicRefine.mli
index 224a7586c..c3ab49e0a 100644
--- a/helm/software/components/cic_unification/cicRefine.mli
+++ b/helm/software/components/cic_unification/cicRefine.mli
@@ -46,3 +46,6 @@ val typecheck :
 
 val insert_coercions: bool ref (* initially true *)
 
+(* given a closed term returns it with all coercions packed *)
+val pack_coercion_obj: Cic.obj -> Cic.obj
+