From 1a685a8dd6747753020b8af3648441a6d7bdf36a Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 18 Nov 2004 16:45:43 +0000 Subject: [PATCH] added set_trust to externally set the trust function (used by the proof checking daemon) --- helm/ocaml/cic_proof_checking/cicEnvironment.ml | 5 +++-- helm/ocaml/cic_proof_checking/cicEnvironment.mli | 3 +++ 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 77d2252eb..0c5c9c01e 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -37,8 +37,9 @@ let cleanup_tmp = true;; -let trust_obj = function uri -> true;; -(*let trust_obj = function uri -> false;;*) +let trust = ref (fun _ -> true);; +let set_trust f = trust := f +let trust_obj uri = !trust uri type type_checked_obj = CheckedObj of Cic.obj (* cooked obj *) diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index 3e5c2bf77..b7b4a5179 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -92,6 +92,9 @@ val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit val empty : unit -> unit +(** Set trust function. Per default this function is set to (fun _ -> true) *) +val set_trust: (UriManager.uri -> bool) -> unit + (* for filtering in tacticChaser *) (* NEW *) val in_cache : UriManager.uri -> bool -- 2.39.2