From 59977ba4636f09f6b2c22c6af9adc5257f2d8a46 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 18 Nov 2005 17:22:50 +0000
Subject: [PATCH] fixed coercions undo

---
 helm/matita/matitaEngine.ml |  6 +++++-
 helm/matita/matitaSync.ml   | 14 +++++++++++---
 helm/matita/matitaTypes.ml  |  1 +
 helm/matita/matitaTypes.mli |  1 +
 4 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 1d3b1f94e..503d4a06a 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -614,8 +614,11 @@ let eval_coercion status coercion =
   let new_coercions =
     CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
   let status =
-   List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status)
+   List.fold_left (fun s (uri,o,_) -> 
+      let status = MatitaSync.add_obj uri o status in
+      {status with coercions = uri :: status.coercions})
     status new_coercions in
+  let status = {status with coercions = coer_uri :: status.coercions} in
   let statement_of name =
     GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, 
       (CicNotationPt.Ident (name, None)))
@@ -1015,6 +1018,7 @@ let initial_status =
     proof_status = No_proof;
     options = default_options ();
     objects = [];
+    coercions = [];
     notation_ids = [];
   }
 
diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index cbf305261..716aa04d2 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -229,13 +229,20 @@ module UriSet = Set.Make (OrderedUri)
 module IdSet  = Set.Make (OrderedId)
 
   (** @return l2 \ l1 *)
-let uri_list_diff l2 l1 =
+let urixstring_list_diff l2 l1 =
   let module S = UriSet in
   let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
   let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
   let diff = S.diff s2 s1 in
   S.fold (fun uri uris -> uri :: uris) diff []
 
+let uri_list_diff l2 l1 =
+  let module S = UriManager.UriSet in
+  let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
+  let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
+  let diff = S.diff s2 s1 in
+  S.fold (fun uri uris -> uri :: uris) diff []
+
   (** @return l2 \ l1 *)
 let id_list_diff l2 l1 =
   let module S = IdSet in
@@ -248,15 +255,16 @@ let remove_coercion uri =
   CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri)
   
 let time_travel ~present ~past =
-  let objs_to_remove = uri_list_diff present.objects past.objects in
+  let objs_to_remove = urixstring_list_diff present.objects past.objects in
+  let coercions_to_remove = uri_list_diff present.coercions past.coercions in
   let notation_to_remove =
     id_list_diff present.notation_ids past.notation_ids
   in
   let debug_list = ref [] in
+  List.iter remove_coercion coercions_to_remove;
   List.iter
     (fun (uri,p) -> 
       MatitaMisc.safe_remove p;
-      remove_coercion uri;
       (try 
         CicEnvironment.remove_obj uri
       with CicEnvironment.Object_not_found _ -> 
diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index df21e09f4..8bd32bb23 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -72,6 +72,7 @@ type status = {
   proof_status: proof_status;
   options: options;
   objects: (UriManager.uri * string) list;
+  coercions: UriManager.uri list;
   notation_ids: CicNotation.notation_id list;
 }
 
diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index f27f2a11b..e54fe5c7e 100644
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -62,6 +62,7 @@ type status = {
   proof_status: proof_status;                             (** logical status *)
   options: options;
   objects: (UriManager.uri * string) list;  (** in-scope objects, with paths *)
+  coercions: UriManager.uri list;                      (** defined coercions *)
   notation_ids: CicNotation.notation_id list;      (** in-scope notation ids *)
 }
 
-- 
2.39.2