diff options
Diffstat (limited to 'pretyping/program.ml')
| -rw-r--r-- | pretyping/program.ml | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/pretyping/program.ml b/pretyping/program.ml index 0bd121f6f1..133f83090e 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -67,3 +67,21 @@ let mk_coq_and l = (fun c conj -> mkApp (and_typ, [| c ; conj |])) l + +(* true = transparent by default, false = opaque if possible *) +let proofs_transparency = ref true + +let set_proofs_transparency = (:=) proofs_transparency +let get_proofs_transparency () = !proofs_transparency + +open Goptions + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "preferred transparency of Program obligations"; + optkey = ["Transparent";"Obligations"]; + optread = get_proofs_transparency; + optwrite = set_proofs_transparency; } + |