objects are typechecked to ensure there is a graph before doing all the stuff......

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index 513612f9beceb4e988e40886644dd768b29d8032..6e2074db0b887120901a5429865567afe84cdc2b 100644 (file)
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -38,7 +38,7 @@ let _ =
       (fun u -> try Some (UriManager.uri_of_string u) with _ -> None) alluris 
   in
   (* brutal *)
-  prerr_endline "loading graphs...";
+  prerr_endline "computing graphs to load...";
   let dbd = HSql.quick_connect (LibraryDb.parse_dbd_conf ()) in
   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
   let uniq l = 
@@ -59,6 +59,13 @@ let _ =
           in
           (fix [] alluris)
   in
+  prerr_endline "generating Coq graphs...";
+  CicEnvironment.set_trust (fun _ -> false);
+  List.iter (fun u ->
+          prerr_endline (" - " ^ UriManager.string_of_uri u);
+          ignore(CicTypeChecker.typecheck u);
+    ) alluris;
+  prerr_endline "loading...";
   List.iter 
     (fun u -> 
        prerr_endline ("  - "^UriManager.string_of_uri u);