X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=8014a19404d99da98716962b039b203ef559e97d;hb=d8b76c102e4f540c3ecfa550267331a7a72810c2;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..8014a1940 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -399,3 +399,9 @@ 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
+;;