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 0f019a6925ac3b3e9ec51b91d6799f530b801c07..ee5d842780bf2a884b2faff3c3cde0b2cee2da46 100644 (file)
--- a/helm/ocaml/grafite2/matitaSync.ml
+++ b/helm/ocaml/grafite2/matitaSync.ml
@@ -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,26 +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 compounds = CoercGraph.add_coercion uri in
- let status = 
-   if add_composites then
-     (List.iter (fun (u,_) -> 
-       prerr_endline (UriManager.string_of_uri u)) compounds;
-     List.fold_left (fun s (uri,o) -> add_obj uri o s) status compounds )
-   else
-     status
- in
- let status = 
-   {status with coercions = uri :: List.map fst compounds @ 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 (List.map fst compounds)
+let add_coercion status uri compounds =
+ let status = {status with coercions = uri :: status.coercions} in
+ List.fold_left add_alias_for_constant status compounds
  
 module OrderedUri =
 struct
@@ -185,13 +165,13 @@ let time_travel ~present ~past =
   in
   let debug_list = ref [] in
   List.iter
-   (fun uri -> CoercGraph.remove_coercion 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 () =
-  CoercGraph.remove_all ();
+  LibrarySync.remove_all_coercions ();
   LibraryObjects.reset_defaults ();
   {
     aliases = DisambiguateTypes.Environment.empty;