universes are written with the URI inside objects, this allows

[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 9c6c53aeef5e2d43465b98e524c21aecb67112ef..d70bd15453cea4b9562d7abf94db97d21eaf94ef 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -159,8 +159,10 @@ let add_single_obj uri obj refinement_toolkit =
       (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n" 
       (univ_time *. 100. /. total_time) (total_time) (univ_time)
       (UriManager.name_of_uri uri));*)
-    let _, ugraph, univlist = 
-      CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
+    let obj, ugraph, univlist = 
+      try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri 
+      with CicEnvironment.Object_not_found _ -> assert false
+    in
     try 
       index_obj ~dbd ~uri; (* 2 must be in the env *)
       try
@@ -228,7 +230,7 @@ let generate_elimination_principles uri refinement_toolkit =
        List.iter remove_single_obj !uris;
        raise exn 
   in
-  let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
+  let obj, _ = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in
     match obj with
       | Cic.InductiveDefinition (indTypes, _, _, _) ->
          let counter = ref 0 in
@@ -272,7 +274,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
 =
   let coer_ty,_ =
     let coer = CicUtil.term_of_uri uri in
-    CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph 
+    CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph 
   in
   (* we have to get the source and the tgt type uri
    * in Coq syntax we have already their names, but
@@ -419,8 +421,8 @@ let generate_projections refinement_toolkit uri fields =
     (fun (uri, name, bo) (_name, coercion, arity) ->
       let saturations = 0 in
       try
-       let ty, ugraph =
-         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
+       let ty, _ =
+         CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_ugraph in
        let attrs = [`Class `Projection; `Generated] in
        let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
         add_single_obj uri obj refinement_toolkit;
@@ -519,21 +521,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;