New tactic: inversion.

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

diff --git a/helm/ocaml/grafite2/matitaSync.mli b/helm/ocaml/grafite2/matitaSync.mli
index df4f111aba65560af6ae2119d4a58b0defd55ad8..bc744f8622215e4f25d5d5dcaa8f7bc36efcc557 100644 (file)
--- 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
+
+