X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.mli;h=30b264455246890438191bc2a1a0a9757db652fa;hb=5f18d404d23d75d47b018631cc05221ccd2d2b1b;hp=c3ab49e0abd84dd19a79de242dffb25999928e79;hpb=185bfc8f9c9ba49308477ee6769701f3e2977115;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.mli b/helm/software/components/cic_unification/cicRefine.mli
index c3ab49e0a..30b264455 100644
--- a/helm/software/components/cic_unification/cicRefine.mli
+++ b/helm/software/components/cic_unification/cicRefine.mli
@@ -46,6 +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
 
+val pack_coercion_metasenv: Cic.metasenv -> Cic.metasenv