From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 18 Nov 2004 16:45:43 +0000 (+0000)
Subject: added set_trust to externally set the trust function (used by the proof
X-Git-Tag: PRE_UNIVERSES~23
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1a685a8dd6747753020b8af3648441a6d7bdf36a;p=helm.git

added set_trust to externally set the trust function (used by the proof
checking daemon)
---

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