fixed undo support for coercions inside records

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

diff --git a/helm/ocaml/grafite2/matitaSync.ml b/helm/ocaml/grafite2/matitaSync.ml
index 26ebbd03224f8e720bec51af988f10df84816e91..ee5d842780bf2a884b2faff3c3cde0b2cee2da46 100644 (file)
--- a/helm/ocaml/grafite2/matitaSync.ml
+++ b/helm/ocaml/grafite2/matitaSync.ml
@@ -56,7 +56,7 @@ let set_proof_aliases status new_aliases =
     (function
     | GrafiteAst.Ident_alias (_, suri) ->
         let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in
-        Some (GrafiteAst.Dependency buri)
+        Some (LibraryNoDb.Dependency buri)
     | _ -> None)
  in
  let aliases =
@@ -75,7 +75,7 @@ let set_proof_aliases status new_aliases =
      DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases
    in
    let status = add_moo_content (commands_of_aliases aliases) new_status in
-   let status = add_moo_metadata (deps_of_aliases aliases) status in
+   let status = add_metadata (deps_of_aliases aliases) status in
    status
 
 (** given a uri and a type list (the contructors types) builds a list of pairs
@@ -114,10 +114,7 @@ let add_aliases_for_object status uri =
   | Cic.Variable _
   | Cic.CurrentProof _ -> assert false
   
-let add_obj uri obj status =
- let basedir = Helm_registry.get "matita.basedir" in
- let lemmas = LibrarySync.add_obj uri obj basedir in
- let status = {status with objects = uri::status.objects} in
+let add_obj uri obj lemmas status =
   List.fold_left add_alias_for_constant
    (add_aliases_for_object status uri obj) lemmas
 
@@ -125,16 +122,9 @@ let add_obj =
  let profiler = HExtlib.profile "add_obj" in
   fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status
 
-let add_coercion status ~add_composites uri =
- let basedir = Helm_registry.get "matita.basedir" in
- let lemmas = CoercGraph.add_coercion ~basedir ~add_composites uri in
+let add_coercion status uri compounds =
  let status = {status with coercions = uri :: status.coercions} in
- let statement_of name =
-  GrafiteAst.Coercion
-   (DisambiguateTypes.dummy_floc, CicUtil.term_of_uri uri, false) in
- let moo_content = [statement_of (UriManager.name_of_uri uri)] in
- let status = GrafiteTypes.add_moo_content moo_content status in
-  List.fold_left add_alias_for_constant status lemmas
+ List.fold_left add_alias_for_constant status compounds
  
 module OrderedUri =
 struct
@@ -175,7 +165,24 @@ let time_travel ~present ~past =
   in
   let debug_list = ref [] in
   List.iter
-   (fun uri -> CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri))
+   (fun uri -> LibrarySync.remove_coercion uri)
    coercions_to_remove;
   List.iter LibrarySync.remove_obj objs_to_remove;
   List.iter CicNotation.remove_notation notation_to_remove
+
+let init () =
+  LibrarySync.remove_all_coercions ();
+  LibraryObjects.reset_defaults ();
+  {
+    aliases = DisambiguateTypes.Environment.empty;
+    multi_aliases = DisambiguateTypes.Environment.empty;
+    moo_content_rev = [];
+    metadata = [];
+    proof_status = No_proof;
+    options = no_options;
+    objects = [];
+    coercions = [];
+    notation_ids = [];
+  }
+
+