X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=0c5c9c01e9030259fff0591ca2a43260e347a84a;hb=1a685a8dd6747753020b8af3648441a6d7bdf36a;hp=77d2252eb330decb5c8b256b185724ec8d428fa9;hpb=9e3da80b505169515fafcbe3ef2438ceb645e35a;p=helm.git 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 *)