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.mli | |
| 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.mli')
| -rw-r--r-- | pretyping/program.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/program.mli b/pretyping/program.mli index b7ebcbc95..765f35580 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -37,3 +37,5 @@ val mk_coq_not : constr -> constr (** Polymorphic application of delayed references *) val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr + +val get_proofs_transparency : unit -> bool |