- cicParser interface changed

- get_obj now has a better behaviour when an unchecked object is retrieved

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index d48ff09bdaa5af533b192c1d304db212d948fc45..329615bb3b5692740033c57c1f3d2f0cf2aebc39 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -153,7 +153,7 @@ let find_or_add_unchecked_to_cache uri =
             (* The body does not exist ==> we consider it an axiom *)
             None
      in
-      let obj = CicParser.obj_of_xml filename bodyfilename uri in
+      let obj = CicParser.obj_of_xml filename bodyfilename in
        if cleanup_tmp then
         begin
          Unix.unlink filename ;
@@ -208,10 +208,14 @@ let get_cooked_obj uri =
   Cache.find_cooked uri
  with Not_found ->
   if not (!trust_obj uri) then
-   prerr_endline ("@@@ OOOOOOOPS: WE TRUST " ^ UriManager.string_of_uri uri ^ " EVEN IF WE SHOULD NOT DO THAT! THAT MEANS LOOKING FOR TROUBLES ;-(") ;
-  match is_type_checked uri with
-     CheckedObj obj -> obj
-   | _ -> assert false
+   begin
+    prerr_endline ("@@@ OOOOOOOPS: WE DO NOT TRUST " ^ UriManager.string_of_uri uri ^ " EVEN IF WE ARE REQUIRED TO DO THAT! THAT MAY MEAN LOOKING FOR TROUBLES ;-(") ;
+    raise Not_found
+   end
+  else
+   match is_type_checked uri with
+      CheckedObj obj -> obj
+    | _ -> assert false
 ;;
 
 (* get_obj uri                                                                *)