From cfa493bfa46cd1628fa8b1490ed1abdcff58d657 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 21 Jun 2016 19:06:46 +0200 Subject: 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. --- pretyping/program.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'pretyping/program.mli') 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 -- cgit v1.2.3