X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=203f78869b33aac4e75c65bb8355e9d9ea485c5d;hb=ac31c84bb9bcf327554976d4296d787853fc8db5;hp=c36d84c90dd88de02938fdef9507906a55659edb;hpb=81d0d5a3aad863b991996c008f5c19076e771dbb;p=helm.git

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index c36d84c90..203f78869 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -169,7 +169,8 @@ let add_single_obj uri obj refinement_toolkit =
         (* EXPERIMENTAL: pretty print the object in natural language *)
 	(try !object_declaration_hook uri obj
 	 with exc ->
-	  prerr_endline "Error: object_declaration_hook failed");
+	  prerr_endline ("Error: object_declaration_hook failed"^
+          Printexc.to_string exc));
         try 
          HLog.message
           (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
@@ -243,6 +244,29 @@ let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
   CoercDb.remove_coercion (fun (_,_,_,_) -> true)
 
+let stack = ref [];;
+
+let h2l h =
+  UriManager.UriHashtbl.fold 
+  (fun k v acc -> (k,v) :: acc) h []
+;;
+
+let push () =
+  stack := (CoercDb.dump (), h2l coercion_hashtbl) :: !stack;
+  remove_all_coercions ()
+;;
+
+let pop () =
+  match !stack with
+  | [] -> raise (Failure "Unable to POP from librarySync.ml")
+  | (db,h) :: tl -> 
+      stack := tl;
+      remove_all_coercions ();
+      CoercDb.restore db;
+      List.iter (fun (k,v) -> UriManager.UriHashtbl.add coercion_hashtbl k v)
+      h
+;;
+
 let add_coercion ~add_composites refinement_toolkit uri arity saturations
  baseuri
 =
@@ -495,21 +519,25 @@ let add_obj refinement_toolkit uri obj =
            generate_sibling_mutual_definitions refinement_toolkit uri attrs
             name bo
     | Cic.Constant _ -> ()
-    | Cic.InductiveDefinition (_,_,_,attrs) ->
-        uris := !uris @ 
-          generate_elimination_principles uri refinement_toolkit;
-        uris := !uris @ generate_inversion refinement_toolkit uri obj;
-        let rec get_record_attrs =
-          function
-          | [] -> None
-          | (`Class (`Record fields))::_ -> Some fields
-          | _::tl -> get_record_attrs tl
-        in
-         (match get_record_attrs attrs with
-         | None -> () (* not a record *)
-         | Some fields ->
-            uris := !uris @ 
-              (generate_projections refinement_toolkit uri fields))
+    | Cic.InductiveDefinition (inductivefuns,_,_,attrs) ->
+       let _,inductive,_,_ = List.hd inductivefuns in
+       if inductive then
+        begin
+         uris := !uris @ 
+           generate_elimination_principles uri refinement_toolkit;
+         uris := !uris @ generate_inversion refinement_toolkit uri obj;
+        end ;
+       let rec get_record_attrs =
+         function
+         | [] -> None
+         | (`Class (`Record fields))::_ -> Some fields
+         | _::tl -> get_record_attrs tl
+       in
+        (match get_record_attrs attrs with
+        | None -> () (* not a record *)
+        | Some fields ->
+           uris := !uris @ 
+             (generate_projections refinement_toolkit uri fields))
     | Cic.CurrentProof _
     | Cic.Variable _ -> assert false
   end;