From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 28 Oct 2002 12:35:49 +0000 (+0000)
Subject: - cicParser interface changed
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=007cfd0ab0b4ce8687f6b94a5810844b3a4c9729;p=helm.git

- 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 d48ff09bd..329615bb3 100644
--- 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                                                                *)