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

3 files changed, 23 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 -> 
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index e06e3e70e1..c1295349da 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