coercions that are marked as variant are unfolded when inserted

[helm.git] / helm / software / components / cic_unification / cicRefine.mli

diff --git a/helm/software/components/cic_unification/cicRefine.mli b/helm/software/components/cic_unification/cicRefine.mli
index 924020cbb39f771bc4bdea179240fd6b7e858432..d17b1ac85b3a46277e476e6e5c3c84455f68af6f 100644 (file)
--- 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