Add option to set the opacity of obligations to transparent, to be able

to reduce proofs (requested by users).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10735 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 20 insertions, 1 deletions

diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index a6639abbcf..c15bfb528c 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 b026e59b23..8ed6ce7e44 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 ->