diff options
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 |