prima implementazione di demodulate, superposition_left e superposition_right

[helm.git] / helm / matita / matitaSync.ml

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index f14e3d1269044d63e15eec3e931c8bc7ab9e1c1b..9a44742b7c5dacebe62d2edd170ccc9020616e61 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -103,7 +103,7 @@ let add_constant ~uri ?body ~ty ~ugraph ?(params = []) ?(attrs = []) status =
     let obj = Cic.Constant (name, body, ty, params, attrs) in
     let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
     CicEnvironment.add_type_checked_term uri (obj, ugraph);
-    MetadataDb.index_constant ~dbd ~uri ~body ~ty;
+    MetadataDb.index_obj ~dbd ~uri; (* must be in the env *)
     let new_stuff = save_object_to_disk status uri obj in  
     MatitaLog.message (sprintf "%s constant defined" suri);
     { status with objects = new_stuff @ status.objects }
@@ -126,7 +126,7 @@ let add_inductive_def
     let obj = Cic.InductiveDefinition (types, params, leftno, attrs) in
     let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
     CicEnvironment.put_inductive_definition uri (obj, ugraph);
-    MetadataDb.index_inductive_def ~dbd ~uri ~types:types;
+    MetadataDb.index_obj ~dbd ~uri; (* must be in the env *)
     let new_stuff = save_object_to_disk status uri obj in
     MatitaLog.message (sprintf "%s inductive type defined" suri);
     let status = { status with objects = new_stuff @ status.objects } in
@@ -170,21 +170,25 @@ let delta_status status1 status2 =
   in
   diff status1.objects status2.objects
 
+let remove_coercion uri = 
+  CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri)
+  
 let time_travel ~present ~past =
   let list_of_objs_to_remove = List.rev (delta_status past present) in
     (* List.rev is just for the debugging code, which otherwise may list both
     * something.ind and something.ind#xpointer ... (ask Enrico :-) *)
   let debug_list = ref [] in
-  List.iter (fun (x,p) -> 
-    remove_object_from_disk x p;
+  List.iter (fun (uri,p) -> 
+    remove_object_from_disk uri p;
+    remove_coercion uri;
     (try 
-      CicEnvironment.remove_obj x
+      CicEnvironment.remove_obj uri
     with CicEnvironment.Object_not_found _ -> 
       MatitaLog.debug
         (sprintf "time_travel removes from cache %s that is not in" 
-          (UriManager.string_of_uri x)));
-    let l = MatitaDb.remove_uri x in
-    debug_list := UriManager.string_of_uri x :: !debug_list @ l) 
+          (UriManager.string_of_uri uri)));
+    let l = MatitaDb.remove_uri uri in
+    debug_list := UriManager.string_of_uri uri :: !debug_list @ l) 
   list_of_objs_to_remove;
   
   (* this is debug code