diff options
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 18 | ||||
| -rw-r--r-- | contrib/subtac/subtac_obligations.mli | 3 | ||||
| -rw-r--r-- | doc/refman/Program.tex | 3 |
3 files changed, 23 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index a6639abbc..c15bfb528 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -59,6 +59,22 @@ let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ()) let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t +(* true = All transparent, false = Opaque if possible *) +let proofs_transparency = ref false + +let set_proofs_transparency = (:=) proofs_transparency +let get_proofs_transparency () = !proofs_transparency + +open Goptions + +let _ = + declare_bool_option + { optsync = true; + optname = "transparency of Program obligations"; + optkey = (SecondaryTable ("Transparent","Obligations")); + optread = get_proofs_transparency; + optwrite = set_proofs_transparency; } + let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type let subst_deps obls deps t = @@ -211,7 +227,7 @@ let declare_obligation obl body = let ce = { const_entry_body = body; const_entry_type = Some obl.obl_type; - const_entry_opaque = obl.obl_opaque; + const_entry_opaque = if get_proofs_transparency () then false else obl.obl_opaque; const_entry_boxed = false} in let constant = Declare.declare_constant obl.obl_name diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index b026e59b2..8ed6ce7e4 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -12,6 +12,9 @@ type progress = (* Resolution status of a program *) val set_default_tactic : Tacexpr.glob_tactic_expr -> unit val default_tactic : unit -> Proof_type.tactic +val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *) +val get_proofs_transparency : unit -> bool + type definition_hook = constant -> unit val add_definition : Names.identifier -> Term.constr -> Term.types -> diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index e06e3e70e..c1295349d 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -212,6 +212,9 @@ tactic is replaced by the default one if not specified. Sets the default obligation solving tactic applied to all obligations automatically, whether to solve them or when starting to prove one, e.g. using {\tt Next}. +\item {\tt Set Transparent Obligations} + Force all obligations to be declared as transparent, otherwise let the + system infer which obligations can be declared opaque. \item {\tt Obligations [of \ident]}\comindex{Obligations} Displays all remaining obligations. \item {\tt Obligation num [of \ident]}\comindex{Obligation} Start the proof of |