compose tactic restore and added nocomposites keyword

[helm.git] / components / library / librarySync.ml

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index c71c24f11c109f46458ceb7c030a8e374b5f0bcf..c36d84c90dd88de02938fdef9507906a55659edb 100644 (file)
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -75,7 +75,9 @@ let save_object_to_disk uri obj ugraph univlist =
   in
   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
   let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
-   if Helm_registry.get_bool "matita.system" then
+   if Helm_registry.get_bool "matita.system" &&
+      not (Helm_registry.get_bool "matita.noinnertypes")
+   then
     let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
      Cic2acic.acic_object_of_cic_object obj 
     in
@@ -316,7 +318,9 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
       (CoercDb.to_list ())
   in
   if not add_composites then
-    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[])
+    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+    UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]);
+    [])
   else
     let new_coercions = 
       CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
@@ -335,14 +339,11 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
     CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
     (* add the composites obj and they eventual lemmas *)
     let lemmas = 
-      if add_composites then
         List.fold_left
           (fun acc (_,tgt,uri,saturations,obj,arity) -> 
             add_single_obj uri obj refinement_toolkit;
              (uri,arity,saturations)::acc) 
           [] new_coercions
-      else
-        []
     in
     (* store that composite_uris are related to uri. the first component is
      * the stuff in the DB while the second is stuff for remove_obj *)
@@ -352,8 +353,8 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
        List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
         composite_uris; 
     *)
-    UriManager.UriHashtbl.add coercion_hashtbl uri 
-      (composite_uris,if add_composites then composite_uris else []);
+    UriManager.UriHashtbl.add 
+      coercion_hashtbl uri (composite_uris,composite_uris);
     (*
     prerr_endline ("lemmas:");
       List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
@@ -371,7 +372,8 @@ let remove_coercion uri =
     List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
       composites_in_db;*)
     UriManager.UriHashtbl.remove coercion_hashtbl uri;
-    CoercDb.remove_coercion (fun (_,_,u,_) -> UriManager.eq uri u);
+    CoercDb.remove_coercion 
+      (fun (_,_,u,_) -> UriManager.eq uri u);
     (* remove from the DB *) 
     List.iter 
       (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
@@ -379,7 +381,7 @@ let remove_coercion uri =
     (* remove composites from the lib *)
     List.iter remove_single_obj composites_in_lib
   with
-    Not_found -> () (* mhh..... *)
+    Not_found -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *)
     
 
 let generate_projections refinement_toolkit uri fields =