From 8a2a631e9c2541e3b1906b5be71ebfd506b7ebf4 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 5 Apr 2004 13:58:54 +0000 Subject: [PATCH] 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 --- helm/ocaml/cic_proof_checking/cicEnvironment.ml | 6 ++++++ helm/ocaml/cic_proof_checking/cicEnvironment.mli | 3 +++ 2 files changed, 9 insertions(+) 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 -- 2.39.2