X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.mli;h=d17b1ac85b3a46277e476e6e5c3c84455f68af6f;hb=16770c377b03dd7690dd2d2533a4981f097ba93b;hp=924020cbb39f771bc4bdea179240fd6b7e858432;hpb=683978a2627cf1ce15673360f26806593d22f7b5;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.mli b/helm/software/components/cic_unification/cicRefine.mli
index 924020cbb..d17b1ac85 100644
--- a/helm/software/components/cic_unification/cicRefine.mli
+++ b/helm/software/components/cic_unification/cicRefine.mli
@@ -45,6 +45,7 @@ val typecheck :
    Cic.obj * Cic.metasenv * CicUniv.universe_graph
 
 val insert_coercions: bool ref (* initially true *)
+val pack_coercions : bool ref
 
 val pack_coercion_obj: Cic.obj -> Cic.obj