From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 5 Apr 2004 13:58:54 +0000 (+0000)
Subject: Added a new function in_cache to cicEnvironemt. It takes an uri
X-Git-Tag: dead_dir_walking~91
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=8a2a631e9c2541e3b1906b5be71ebfd506b7ebf4;p=helm.git

Added a new function in_cache to cicEnvironemt. It takes an uri
and returns true or false according to the fact that uri is or
is not in the cache
---

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
+;;
diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index 99244f47f..615cdf9be 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
@@ -83,3 +83,6 @@ val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit
 val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit
 val empty : unit -> unit
 
+(* for filtering in tacticChaser *)
+(* NEW *)
+val in_cache : UriManager.uri -> bool