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.

6 files changed, 72 insertions, 51 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b8fb61e35..205a199f7 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 c168e070f..cba28f817 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 0bd121f6f..133f83090 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 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
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 8a3ea5396..369c59cf2 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -40,7 +40,7 @@ let check_evars env evm =
 type oblinfo =
   { ev_name: int * Id.t;
     ev_hyps: Context.Named.t;
-    ev_status: Evar_kinds.obligation_definition_status;
+    ev_status: bool * Evar_kinds.obligation_definition_status;
     ev_chop: int option;
     ev_src: Evar_kinds.t Loc.located;
     ev_typ: types;
@@ -215,16 +215,20 @@ let eterm_obligations env name evm fs ?status t ty =
 	   | None -> evtyp, hyps, 0
 	 in
 	 let loc, k = evar_source id evm in
-	 let status = match k with Evar_kinds.QuestionMark o -> Some o | _ -> status in
-	 let status, chop = match status with
-	   | Some (Evar_kinds.Define true as stat) ->
-	       if not (Int.equal chop fs) then Evar_kinds.Define false, None
-	       else stat, Some chop
-	   | Some s -> s, None
-	   | None -> Evar_kinds.Define true, None
+	 let status = match k with
+           | Evar_kinds.QuestionMark o -> o
+           | _ -> match status with
+                 | Some o -> o
+                 | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))
+         in
+         let force_status, status, chop = match status with
+	   | Evar_kinds.Define true as stat ->
+	      if not (Int.equal chop fs) then true, Evar_kinds.Define false, None
+	      else false, stat, Some chop
+	   | s -> false, s, None
 	 in
 	 let info = { ev_name = (n, nstr);
-		      ev_hyps = hyps; ev_status = status; ev_chop = chop;
+		      ev_hyps = hyps; ev_status = force_status, status; ev_chop = chop;
 		      ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = None }
 	 in (id, info) :: l)
       evn []
@@ -235,14 +239,14 @@ let eterm_obligations env name evm fs ?status t ty =
   let ty, _, _ = subst_evar_constr evts 0 mkVar ty in
   let evars = 
     List.map (fun (ev, info) ->
-      let { ev_name = (_, name); ev_status = status;
+      let { ev_name = (_, name); ev_status = force_status, status;
 	    ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
       in
-      let status = match status with
+      let force_status, status = match status with
 	| Evar_kinds.Define true when Id.Set.mem name transparent ->
-	  Evar_kinds.Define false
-	| _ -> status
-      in name, typ, src, status, deps, tac) evts
+	  true, Evar_kinds.Define false
+	| _ -> force_status, status
+      in name, typ, src, (force_status, status), deps, tac) evts
   in
   let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
   let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
@@ -268,7 +272,8 @@ let explain_no_obligations = function
 
 type obligation_info =
     (Names.Id.t * Term.types * Evar_kinds.t Loc.located *
-     Evar_kinds.obligation_definition_status * Int.Set.t * unit Proofview.tactic option) array
+       (bool * Evar_kinds.obligation_definition_status)
+       * Int.Set.t * unit Proofview.tactic option) array
 
 type 'a obligation_body = 
   | DefinedObl of 'a
@@ -279,7 +284,7 @@ type obligation =
     obl_type : types;
     obl_location : Evar_kinds.t Loc.located;
     obl_body : constant obligation_body option;
-    obl_status : Evar_kinds.obligation_definition_status;
+    obl_status : bool * Evar_kinds.obligation_definition_status;
     obl_deps : Int.Set.t;
     obl_tac : unit Proofview.tactic option;
   }
@@ -321,29 +326,13 @@ let assumption_message = Declare.assumption_message
 
 let default_tactic = ref (Proofview.tclUNIT ())
 
-(* true = All transparent, 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  = "transparency of Program obligations";
-      optkey   = ["Transparent";"Obligations"];
-      optread  = get_proofs_transparency;
-      optwrite = set_proofs_transparency; }
-
 (* true = hide obligations *)
 let hide_obligations = ref false
 
 let set_hide_obligations = (:=) hide_obligations
 let get_hide_obligations () = !hide_obligations
 
+open Goptions
 let _ =
   declare_bool_option
     { optsync  = true;
@@ -383,7 +372,7 @@ let get_obligation_body expand obl =
   match get_body obl with
   | None -> None
   | Some c ->
-     if expand && obl.obl_status == Evar_kinds.Expand then
+     if expand && snd obl.obl_status == Evar_kinds.Expand then
        match c with
        | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc)
        | TermObl c -> Some c
@@ -608,9 +597,9 @@ let declare_obligation prg obl body ty uctx =
   let body = prg.prg_reduce body in
   let ty = Option.map prg.prg_reduce ty in
   match obl.obl_status with
-  | Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) }
-  | Evar_kinds.Define opaque ->
-      let opaque = if get_proofs_transparency () then false else opaque in
+  | _, Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) }
+  | force, Evar_kinds.Define opaque ->
+      let opaque = not force && opaque in
       let poly = pi2 prg.prg_kind in
       let ctx, body, args =
 	if get_shrink_obligations () && not poly then
@@ -648,7 +637,7 @@ let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
 	let n = Nameops.add_suffix n "_obligation" in
 	  [| { obl_name = n; obl_body = None;
 	       obl_location = Loc.ghost, Evar_kinds.InternalHole; obl_type = t;
-	       obl_status = Evar_kinds.Expand; obl_deps = Int.Set.empty;
+	       obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty;
 	       obl_tac = None } |],
 	mkVar n
     | Some b ->
@@ -816,7 +805,7 @@ let obligation_terminator name num guard hook auto pf =
       let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in
       let env = Global.env () in
       let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
-      let ty = entry.Entries.const_entry_type  in
+      let ty = entry.Entries.const_entry_type in
       let (body, cstr), eff = Future.force entry.Entries.const_entry_body in
       assert(Safe_typing.empty_private_constants = eff);
       let sigma = Evd.from_ctx (fst uctx) in
@@ -828,6 +817,15 @@ let obligation_terminator name num guard hook auto pf =
       let prg = { prg with prg_ctx = ctx } in
       let obls, rem = prg.prg_obligations in
       let obl = obls.(num) in
+      let status =
+        match obl.obl_status, opq with
+        | (_, Evar_kinds.Expand), Vernacexpr.Opaque _ -> err_not_transp ()
+        | (true, _), Vernacexpr.Opaque _ -> err_not_transp ()
+        | (false, _), Vernacexpr.Opaque _ -> Evar_kinds.Define true
+        | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false
+        | (_, status), Vernacexpr.Transparent -> status
+      in
+      let obl = { obl with obl_status = false, status } in
       let uctx = Evd.evar_context_universe_context ctx in
       let (def, obl) = declare_obligation prg obl body ty uctx in
       let obls = Array.copy obls in
@@ -850,9 +848,11 @@ let obligation_hook prg obl num auto ctx' _ gr =
   let cst = match gr with ConstRef cst -> cst | _ -> assert false in
   let transparent = evaluable_constant cst (Global.env ()) in
   let () = match obl.obl_status with
-  | Evar_kinds.Expand -> if not transparent then err_not_transp ()
-  | Evar_kinds.Define op -> if not op && not transparent then err_not_transp ()
-  in
+      (true, Evar_kinds.Expand) 
+    | (true, Evar_kinds.Define true) ->
+       if not transparent then err_not_transp ()
+    | _ -> ()
+in
   let obl = { obl with obl_body = Some (DefinedObl cst) } in
   let () = if transparent then add_hint true prg cst in
   let obls = Array.copy obls in
@@ -893,7 +893,7 @@ let rec solve_obligation prg num tac =
         ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining));
   in
   let obl = subst_deps_obl obls obl in
-  let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
+  let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in
   let evd = Evd.from_ctx prg.prg_ctx in
   let evd = Evd.update_sigma_env evd (Global.env ()) in
   let auto n tac oblset = auto_solve_obligations n ~oblset tac in
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 3e99f5760..69d206961 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -33,7 +33,8 @@ val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar
    evars contexts, object and type *)
 val eterm_obligations : env -> Id.t -> evar_map -> int ->
   ?status:Evar_kinds.obligation_definition_status -> constr -> types ->
-  (Id.t * types * Evar_kinds.t Loc.located * Evar_kinds.obligation_definition_status * Int.Set.t *
+  (Id.t * types * Evar_kinds.t Loc.located *
+     (bool * Evar_kinds.obligation_definition_status) * Int.Set.t *
       unit Proofview.tactic option) array
     (* Existential key, obl. name, type as product, 
        location of the original evar, associated tactic,
@@ -46,7 +47,7 @@ val eterm_obligations : env -> Id.t -> evar_map -> int ->
 
 type obligation_info =
   (Id.t * Term.types * Evar_kinds.t Loc.located *
-      Evar_kinds.obligation_definition_status * Int.Set.t * unit Proofview.tactic option) array
+      (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array
     (* ident, type, location, (opaque or transparent, expand or define),
        dependencies, tactic to solve it *)
 
@@ -57,9 +58,6 @@ type progress = (* Resolution status of a program *)
 
 val default_tactic : unit Proofview.tactic ref
 
-val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
-val get_proofs_transparency : unit -> bool
-
 val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> 
   Evd.evar_universe_context ->
   ?pl:(Id.t Loc.located list) -> (* Universe binders *)