added set_trust to externally set the trust function (used by the proof

[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.mli

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index 3e5c2bf77c161b071c77f80366047b076f8422e1..b7b4a51797c5e9ad34d50c9e7da003521e1f289a 100644 (file)
--- 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