Big commit to let Ferruccio try the merge_coercion patch.

[helm.git] / helm / ocaml / cic_unification / cicRefine.mli

diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli
index 97417f7f673612163e2bc718264a023792557ea7..224a7586c957dfbf91e4704917489a348158b43a 100644 (file)
--- 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 *)
+