X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=e15186fdecdb489f437d50c91bbad63b3e54e00c;hb=0c6a5aadb1a7746681a8e26fc0b009f847c10557;hp=45c0dba5a8b404fbe2201e8e9a0ff24b638340c4;hpb=98295941bee765a0cb4070eb3f2df553228c11c8;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 45c0dba5a..e15186fde 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -38,6 +38,7 @@
 let cleanup_tmp = true;;
 
 let trust_obj = function uri -> true;;
+(*let trust_obj = function uri -> false;;*)
 
 type type_checked_obj =
    CheckedObj of Cic.obj     (* cooked obj *)
@@ -317,7 +318,9 @@ 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 ();
        if cleanup_tmp then
         begin
          Unix.unlink filename ;
@@ -399,3 +402,17 @@ let put_inductive_definition uri obj =
     Cic.InductiveDefinition _ -> Cache.add_cooked uri obj
   | _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed
 ;;
+
+let in_cache uri = 
+ try
+  ignore (Cache.find_cooked uri);true
+ with Not_found -> false
+;;
+
+let add_type_checked_term uri obj =
+  match obj with 
+  Cic.Constant (s,(Some bo),ty,ul) ->
+    Cache.add_cooked ~key:uri obj
+  | _ -> assert false 
+  Cache.add_cooked 
+;;