From 007cfd0ab0b4ce8687f6b94a5810844b3a4c9729 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 28 Oct 2002 12:35:49 +0000 Subject: [PATCH] - cicParser interface changed - get_obj now has a better behaviour when an unchecked object is retrieved --- helm/ocaml/cic_proof_checking/cicEnvironment.ml | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) 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 *) -- 2.39.2