diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-06-21 19:06:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-27 23:29:16 +0200 |
| commit | cfa493bfa46cd1628fa8b1490ed1abdcff58d657 (patch) | |
| tree | 9307dec22eaa1ac2739863e675e28fd00623df34 /pretyping/program.ml | |
| parent | fb4ccbf4a7b66cc7af8b24e00fb19a0b49c769d1 (diff) | |
Rework treatment of default transparency of obligations
By default obligations defined by tactics are defined
transparently or opaque according to the Obligations Transparent flag,
except proofs of subset obligations which are treated
as opaque by default. When the user proves the obligation using
Qed or Defined, this information takes precedence, and only
when the obligation cannot be Qed'ed because it contains
references to a recursive function an error is raised
(this prevents the guardness checker error).
Shrinked obligations were not doings this correctly.
Forcing transparency due to fixpoint prototypes
takes precedence over the user preference.
Program: do not force opacity of subset proofs,
maintaining compatibility.
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 0bd121f6f..133f83090 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; } + |