X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite2%2FmatitaSync.mli;h=bc744f8622215e4f25d5d5dcaa8f7bc36efcc557;hb=059c1bb4766e823aa53b39fed7d3dd55b4a06101;hp=df4f111aba65560af6ae2119d4a58b0defd55ad8;hpb=a58d25c192ff13ecee2cb92f07ee6f1cbe5219b5;p=helm.git

diff --git a/helm/ocaml/grafite2/matitaSync.mli b/helm/ocaml/grafite2/matitaSync.mli
index df4f111ab..bc744f862 100644
--- a/helm/ocaml/grafite2/matitaSync.mli
+++ b/helm/ocaml/grafite2/matitaSync.mli
@@ -24,11 +24,11 @@
  *)
 
 val add_obj:
-  UriManager.uri -> Cic.obj -> 
+  UriManager.uri -> Cic.obj -> UriManager.uri list -> 
     GrafiteTypes.status -> GrafiteTypes.status
 
 val add_coercion:
- GrafiteTypes.status -> add_composites:bool -> UriManager.uri ->
+ GrafiteTypes.status -> UriManager.uri -> UriManager.uri list ->
   GrafiteTypes.status
 
 val time_travel: 
@@ -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
+
+