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/coercion.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/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index c168e070f..cba28f817 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -90,8 +90,9 @@ let inh_pattern_coerce_to loc env pat ind1 ind2 = open Program -let make_existential loc ?(opaque = Evar_kinds.Define true) env evdref c = - Evarutil.e_new_evar env evdref ~src:(loc, Evar_kinds.QuestionMark opaque) c +let make_existential loc ?(opaque = not (get_proofs_transparency ())) env evdref c = + let src = (loc, Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in + Evarutil.e_new_evar env evdref ~src c let app_opt env evdref f t = whd_betaiota !evdref (app_opt f t) |