X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.mli;h=224a7586c957dfbf91e4704917489a348158b43a;hb=f4f050696e66b8604d9f0ff8173afe03addf74d6;hp=97417f7f673612163e2bc718264a023792557ea7;hpb=8d8ac4a42998970114e43c2fb13ff2c98f7c259a;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli
index 97417f7f6..224a7586c 100644
--- a/helm/ocaml/cic_unification/cicRefine.mli
+++ b/helm/ocaml/cic_unification/cicRefine.mli
@@ -43,3 +43,6 @@ val typecheck :
  localization_tbl:Token.flocation Cic.CicHash.t ->
   Cic.metasenv -> UriManager.uri option -> Cic.obj ->
    Cic.obj * Cic.metasenv * CicUniv.universe_graph
+
+val insert_coercions: bool ref (* initially true *)
+