Big commit to let Ferruccio try the merge_coercion patch.

[helm.git] / helm / ocaml / grafite2 / matitaSync.mli

diff --git a/helm/ocaml/grafite2/matitaSync.mli b/helm/ocaml/grafite2/matitaSync.mli
index df4f111aba65560af6ae2119d4a58b0defd55ad8..6161a6a0d96189bdcb7dab983913a66423d1205b 100644 (file)
--- a/helm/ocaml/grafite2/matitaSync.mli
+++ b/helm/ocaml/grafite2/matitaSync.mli
@@ -47,3 +47,8 @@ val set_proof_aliases :
   GrafiteTypes.status ->
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list ->
   GrafiteTypes.status
+
+  (* also resets the imperative part of the status *)
+val init: unit -> GrafiteTypes.status
+
+