X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=d214d89b5cf0be3157fc252e2199eec5da3968d5;hb=2a8397bf2db45db960899499fb59183a68778248;hp=e15186fdecdb489f437d50c91bbad63b3e54e00c;hpb=e51a16c072144e4cabc8fc70841aa4e94a9325b6;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index e15186fde..d214d89b5 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -318,16 +318,25 @@ let find_or_add_unchecked_to_cache uri =
             (* The body does not exist ==> we consider it an axiom *)
             None
      in
-      CicUniv.directly_to_env_begin ();
-      let obj = CicParser.obj_of_xml filename bodyfilename in
-      CicUniv.directly_to_env_end ();
+     let cleanup () =
        if cleanup_tmp then
         begin
-         Unix.unlink filename ;
+         if Sys.file_exists filename then Unix.unlink filename ;
          match bodyfilename with
-            Some f -> Unix.unlink f
+            Some f -> if Sys.file_exists f then Unix.unlink f
           | None -> ()
         end ;
+      in
+      CicUniv.directly_to_env_begin ();
+      let obj =
+        try
+          CicParser.obj_of_xml filename bodyfilename
+        with exn ->
+          cleanup ();
+          raise exn
+      in
+      CicUniv.directly_to_env_end ();
+      cleanup ();
        obj
    )
 ;;