call Unshare.fresh_types

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

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 630b51be8a59c4352cf4fe92bbf5d716f6891d1f..8a0c2bcc4406f8832a2fbe0e6fac5300ee4232ba 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -128,7 +128,8 @@ let save_object_to_disk uri obj ugraph univlist =
 
 let typecheck_obj =
  let profiler = HExtlib.profile "add_obj.typecheck_obj" in
-  fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
+  fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri)
+  (Unshare.fresh_types obj)
 
 let index_obj =
  let profiler = HExtlib.profile "add_obj.index_obj" in
@@ -169,7 +170,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))
@@ -518,21 +520,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;