diff options
| author | Matthieu Sozeau | 2016-06-21 19:06:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-27 23:29:16 +0200 |
| commit | cfa493bfa46cd1628fa8b1490ed1abdcff58d657 (patch) | |
| tree | 9307dec22eaa1ac2739863e675e28fd00623df34 /pretyping | |
| 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')
| -rw-r--r-- | pretyping/cases.ml | 4 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 5 | ||||
| -rw-r--r-- | pretyping/program.ml | 18 | ||||
| -rw-r--r-- | pretyping/program.mli | 2 |
4 files changed, 26 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b8fb61e35d..205a199f7f 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2032,7 +2032,9 @@ let mk_JMeq evdref typ x typ' y = let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] -let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true), Misctypes.IntroAnonymous, None) +let hole = + GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false), + Misctypes.IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = let rec typ env (ty, realargs) pat avoid = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index c168e070f2..cba28f817b 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) 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; } + diff --git a/pretyping/program.mli b/pretyping/program.mli index b7ebcbc95c..765f355808 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 |