From bd55e2b2787bbabf7fba126126611c58548424fc Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 16 Jun 2016 18:49:07 +0200
Subject: Shrink Proofs/Obligations by default and deprecate

Fix bug in Shrink obligations with Program in the process.

Fix implementation of shrink for abstract proofs

- Update doc in term.mli to reflect the fact that let-in's
  are part of what is returned by [decompose_lam_assum].
---
 kernel/term.mli               |   2 +-
 tactics/tactics.ml            |   6 +-
 test-suite/bugs/closed/1784.v |   5 +-
 toplevel/obligations.ml       | 132 +++++++++++++++++++++++-------------------
 4 files changed, 80 insertions(+), 65 deletions(-)

diff --git a/kernel/term.mli b/kernel/term.mli
index 32267f6c4c..60a3c77154 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -315,7 +315,7 @@ val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr
    "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *)
 val decompose_prod_assum : types -> Context.Rel.t * types
 
-(** Idem with lambda's *)
+(** Idem with lambda's and let's *)
 val decompose_lam_assum : constr -> Context.Rel.t * constr
 
 (** Idem but extract the first [n] premisses, counting let-ins. *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e264505314..f3e117f8c3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -119,12 +119,12 @@ let _ =
 
 (* Shrinking of abstract proofs. *)
 
-let shrink_abstract = ref false
+let shrink_abstract = ref true
 
 let _ =
   declare_bool_option
     { optsync  = true;
-      optdepr  = false;
+      optdepr  = true;
       optname  = "shrinking of abstracted proofs";
       optkey   = ["Shrink"; "Abstract"];
       optread  = (fun () -> !shrink_abstract) ;
@@ -4774,7 +4774,7 @@ let rec shrink ctx sign c t accu =
   match ctx, sign with
   | [], [] -> (c, t, accu)
   | p :: ctx, decl :: sign ->
-      if noccurn 1 c then
+      if noccurn 1 c && noccurn 1 t then
         let c = subst1 mkProp c in
         let t = subst1 mkProp t in
         shrink ctx sign c t accu
diff --git a/test-suite/bugs/closed/1784.v b/test-suite/bugs/closed/1784.v
index 0b63d7b567..25d1b192eb 100644
--- a/test-suite/bugs/closed/1784.v
+++ b/test-suite/bugs/closed/1784.v
@@ -91,9 +91,8 @@ Next Obligation. intro H; inversion H. Defined.
 Next Obligation. intro H; inversion H; subst. Defined.
 Next Obligation.
   intro H1; contradict H. inversion H1; subst. assumption.
-  contradict H0; assumption. Defined.
-Next Obligation. 
-  intro H1; contradict H0. inversion H1; subst. assumption. Defined.
+  contradict H0; assumption.  Defined.
+Next Obligation. intro H1; contradict H0. inversion H1; subst. assumption. Defined.
 Next Obligation.
   intro H1; contradict H. inversion H1; subst. assumption. Defined.
 Next Obligation.
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index ccc8e2ffea..8a3ea53966 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -353,7 +353,7 @@ let _ =
       optread  = get_hide_obligations;
       optwrite = set_hide_obligations; }
 
-let shrink_obligations = ref false
+let shrink_obligations = ref true
 
 let set_shrink_obligations = (:=) shrink_obligations
 let get_shrink_obligations () = !shrink_obligations
@@ -361,7 +361,7 @@ let get_shrink_obligations () = !shrink_obligations
 let _ =
   declare_bool_option
     { optsync  = true;
-      optdepr  = false;
+      optdepr  = true;
       optname  = "Shrinking of Program obligations";
       optkey   = ["Shrink";"Obligations"];
       optread  = get_shrink_obligations;
@@ -369,36 +369,35 @@ let _ =
 
 let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
 
-let get_body obl = 
+let get_body obl =
   match obl.obl_body with
-  | None -> assert false
+  | None -> None
   | Some (DefinedObl c) ->
     let ctx = Environ.constant_context (Global.env ()) c in
     let pc = (c, Univ.UContext.instance ctx) in
-      DefinedObl pc
-  | Some (TermObl c) -> 
-      TermObl c
+      Some (DefinedObl pc)
+  | Some (TermObl c) ->
+      Some (TermObl c)
 
 let get_obligation_body expand obl =
-  let c = get_body obl in
-  let c' = 
-    if expand && obl.obl_status == Evar_kinds.Expand then
-      (match c with
-      | DefinedObl pc -> constant_value_in (Global.env ()) pc
-      | TermObl c -> c)
-    else (match c with
-    | DefinedObl pc -> mkConstU pc
-    | TermObl c -> c)
-  in c'
+  match get_body obl with
+  | None -> None
+  | Some c ->
+     if expand && obl.obl_status == Evar_kinds.Expand then
+       match c with
+       | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc)
+       | TermObl c -> Some c
+     else (match c with
+	   | DefinedObl pc -> Some (mkConstU pc)
+	   | TermObl c -> Some c)
 
 let obl_substitution expand obls deps =
   Int.Set.fold
     (fun x acc ->
        let xobl = obls.(x) in
-       let oblb =
-	 try get_obligation_body expand xobl
-	 with e when Errors.noncritical e -> assert false
-       in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
+       match get_obligation_body expand xobl with
+       | None -> acc
+       | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
     deps []
 
 let subst_deps expand obls deps t =
@@ -590,9 +589,9 @@ let declare_mutual_definition l =
 let shrink_body c =
   let open Context.Rel.Declaration in
   let ctx, b = decompose_lam_assum c in
-  let b', n, args = 
+  let b', n, args =
     List.fold_left (fun (b, i, args) decl ->
-      if noccurn 1 b then 
+      if noccurn 1 b then
 	subst1 mkProp b, succ i, args
       else
 	let args = if is_local_assum decl then mkRel i :: args else args in
@@ -613,12 +612,12 @@ let declare_obligation prg obl body ty uctx =
   | Evar_kinds.Define opaque ->
       let opaque = if get_proofs_transparency () then false else opaque in
       let poly = pi2 prg.prg_kind in
-      let ctx, body, args = 
+      let ctx, body, args =
 	if get_shrink_obligations () && not poly then
-	  shrink_body body else [], body, [||] 
+	  shrink_body body else [], body, [||]
       in
       let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
-      let ce = 
+      let ce =
         { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
           const_entry_secctx = None;
 	  const_entry_type = if List.is_empty ctx then ty else None;
@@ -628,21 +627,21 @@ let declare_obligation prg obl body ty uctx =
           const_entry_inline_code = false;
           const_entry_feedback = None;
       } in
-    (** ppedrot: seems legit to have obligations as local *)
+      (** ppedrot: seems legit to have obligations as local *)
       let constant = Declare.declare_constant obl.obl_name ~local:true
 	(DefinitionEntry ce,IsProof Property)
       in
 	if not opaque then add_hint false prg constant;
 	definition_message obl.obl_name;
 	true, { obl with obl_body =
-	    if poly then 
+	    if poly then
 	      Some (DefinedObl constant)
 	    else
 	      Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
 
 let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
 		   notations obls impls kind reduce hook =
-  let obls', b = 
+  let obls', b =
     match b with
     | None ->
 	assert(Int.equal (Array.length obls) 0);
@@ -806,7 +805,7 @@ let solve_by_tac name evi t poly ctx =
   Inductiveops.control_only_guard (Global.env ()) (fst body);
   (fst body), entry.const_entry_type, Evd.evar_universe_context ctx'
 
-let obligation_terminator name num guard hook pf =
+let obligation_terminator name num guard hook auto pf =
   let open Proof_global in
   let term = Lemmas.universe_proof_terminator guard hook in
   match pf with
@@ -820,18 +819,28 @@ let obligation_terminator name num guard hook pf =
       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);
-      assert(Univ.ContextSet.is_empty cstr);
+      let sigma = Evd.from_ctx (fst uctx) in
+      let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
       Inductiveops.control_only_guard (Global.env ()) body;
       (** Declare the obligation ourselves and drop the hook *)
       let prg = get_info (ProgMap.find name !from_prg) in
-      let prg = { prg with prg_ctx = fst uctx } in
+      let ctx = Evd.evar_universe_context sigma in
+      let prg = { prg with prg_ctx = ctx } in
       let obls, rem = prg.prg_obligations in
       let obl = obls.(num) in
-      let ctx = Evd.evar_context_universe_context (fst uctx) in
-      let (_, obl) = declare_obligation prg obl body ty ctx 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
       let _ = obls.(num) <- obl in
-      try ignore (update_obls prg obls (pred rem))
+      try
+      ignore (update_obls prg obls (pred rem));
+      if def then
+        if pred rem > 0 then
+          begin
+	    let deps = dependencies obls num in
+	    if not (Int.Set.is_empty deps) then
+	    ignore (auto (Some name) None deps)
+	  end
       with e when Errors.noncritical e ->
         let e = Errors.push e in
         pperror (Errors.iprint (Cerrors.process_vernac_interp_error e))
@@ -888,7 +897,9 @@ let rec solve_obligation prg num tac =
   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
-  let terminator guard hook = Proof_global.make_terminator (obligation_terminator prg.prg_name num guard hook) in
+  let terminator guard hook =
+    Proof_global.make_terminator
+      (obligation_terminator prg.prg_name num guard hook auto) in
   let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
   let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator hook in
   let _ = Pfedit.by !default_tactic in
@@ -909,7 +920,7 @@ and obligation (user_num, name, typ) tac =
 and solve_obligation_by_tac prg obls i tac =
   let obl = obls.(i) in
     match obl.obl_body with
-    | Some _ -> false
+    | Some _ -> None
     | None ->
 	try
 	  if List.is_empty (deps_remaining obls obl.obl_deps) then
@@ -922,30 +933,30 @@ and solve_obligation_by_tac prg obls i tac =
 		  | Some t -> t
 		  | None -> !default_tactic
 	    in
-	    let evd = Evd.from_ctx !prg.prg_ctx in
+	    let evd = Evd.from_ctx prg.prg_ctx in
 	    let evd = Evd.update_sigma_env evd (Global.env ()) in
-	    let t, ty, ctx = 
-	      solve_by_tac obl.obl_name (evar_of_obligation obl) tac 
-	        (pi2 !prg.prg_kind) (Evd.evar_universe_context evd)
+	    let t, ty, ctx =
+	      solve_by_tac obl.obl_name (evar_of_obligation obl) tac
+	        (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
 	    in
 	    let uctx = Evd.evar_context_universe_context ctx in
-	    let () = prg := {!prg with prg_ctx = ctx} in
-	    let def, obl' = declare_obligation !prg obl t ty uctx in
+	    let prg = {prg with prg_ctx = ctx} in
+	    let def, obl' = declare_obligation prg obl t ty uctx in
 	      obls.(i) <- obl';
-	      if def && not (pi2 !prg.prg_kind) then (
+	      if def && not (pi2 prg.prg_kind) then (
 	        (* Declare the term constraints with the first obligation only *)
 	        let evd = Evd.from_env (Global.env ()) in
 	        let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in
 		let ctx' = Evd.evar_universe_context evd in
-		  prg := {!prg with prg_ctx = ctx'});
-	      true
-	  else false
+		  Some {prg with prg_ctx = ctx'})
+	      else Some prg
+	  else None
 	with e when Errors.noncritical e ->
           let (e, _) = Errors.push e in
           match e with
 	  | Refiner.FailError (_, s) ->
 	      user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
-          | e -> false
+          | e -> None (* FIXME really ? *)
 
 and solve_prg_obligations prg ?oblset tac =
   let obls, rem = prg.prg_obligations in
@@ -957,16 +968,20 @@ and solve_prg_obligations prg ?oblset tac =
     | Some s -> set := s;
       (fun i -> Int.Set.mem i !set)
   in
-  let prg = ref prg in
+  let prgref = ref prg in
   let _ =
     Array.iteri (fun i x ->
-      if p i && solve_obligation_by_tac prg obls' i tac then
- 	let deps = dependencies obls i in
- 	  (set := Int.Set.union !set deps;
- 	   decr rem))
+      if p i then
+        match solve_obligation_by_tac !prgref obls' i tac with
+	| None -> ()
+ 	| Some prg' ->
+	   prgref := prg';
+	   let deps = dependencies obls i in
+ 	   (set := Int.Set.union !set deps;
+ 	    decr rem))
       obls'
   in
-    update_obls !prg obls' !rem
+    update_obls !prgref obls' !rem
 
 and solve_obligations n tac =
   let prg = get_prog_err n in
@@ -979,9 +994,9 @@ and try_solve_obligation n prg tac =
   let prg = get_prog prg in
   let obls, rem = prg.prg_obligations in
   let obls' = Array.copy obls in
-  let prgref = ref prg in
-    if solve_obligation_by_tac prgref obls' n tac then
-      ignore(update_obls !prgref obls' (pred rem));
+    match solve_obligation_by_tac prg obls' n tac with
+    | Some prg' -> ignore(update_obls prg' obls' (pred rem))
+    | None -> ()
 
 and try_solve_obligations n tac =
   try ignore (solve_obligations n tac) with NoObligations _ -> ()
@@ -1000,7 +1015,8 @@ let show_obligations_of_prg ?(msg=true) prg =
 		   match x.obl_body with
 		   | None ->
 		       if !showed > 0 then (
-			 decr showed;
+		         decr showed;
+			 let x = subst_deps_obl obls x in
 			 Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
 				   str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++
 				   hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++
-- 
cgit v1.2.3


From fb4ccbf4a7b66cc7af8b24e00fb19a0b49c769d1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 20 Jun 2016 20:21:27 +0200
Subject: Add Unset Shrink Abstract/Obligations in Coq85

For compatibility with 8.5.
---
 theories/Compat/Coq85.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index d6d370cb51..1e30ab9197 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -15,3 +15,5 @@
 Global Unset Bracketing Last Introduction Pattern.
 Global Unset Regular Subst Tactic.
 Global Unset Structural Injection.
+Global Unset Shrink Abstract.
+Global Unset Shrink Obligations.
\ No newline at end of file
-- 
cgit v1.2.3


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/cases.ml       |  4 ++-
 pretyping/coercion.ml    |  5 +--
 pretyping/program.ml     | 18 ++++++++++
 pretyping/program.mli    |  2 ++
 toplevel/obligations.ml  | 86 ++++++++++++++++++++++++------------------------
 toplevel/obligations.mli |  8 ++---
 6 files changed, 72 insertions(+), 51 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b8fb61e35d..205a199f7f 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 c168e070f2..cba28f817b 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 0bd121f6f1..133f83090e 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 b7ebcbc95c..765f355808 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 8a3ea53966..369c59cf29 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 3e99f5760b..69d2069616 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 *)
-- 
cgit v1.2.3


From 4a957f05970f352ad8e40b47918bd9812b5a8fd2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 23 Jun 2016 15:54:28 +0200
Subject: Program: refine shrinking of obligations

Ensure correspondence between the term and type to shrink, so that Lets
are preserved when they are used relevantly in either of them.  This
avoids e.g. "simpl" in the shrinked hypotheses to reduce shrinking,
while maintaining unsimplified types in the type of the shrinked
obligations (for compatibility).
Simplify Lambda, Prod case of shrinking,
By invariant (we start with a term and its type), the abstraction's
types correspond.
---
 toplevel/obligations.ml | 59 +++++++++++++++++++++++++++++++++++++------------
 1 file changed, 45 insertions(+), 14 deletions(-)

diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 369c59cf29..bea96d0b78 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -575,18 +575,49 @@ let declare_mutual_definition l =
     Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
     List.iter progmap_remove l; kn
 
-let shrink_body c =
+let decompose_lam_prod c ty =
   let open Context.Rel.Declaration in
-  let ctx, b = decompose_lam_assum c in
-  let b', n, args =
-    List.fold_left (fun (b, i, args) decl ->
-      if noccurn 1 b then
-	subst1 mkProp b, succ i, args
-      else
-	let args = if is_local_assum decl then mkRel i :: args else args in
-        mkLambda_or_LetIn decl b, succ i, args)
-     (b, 1, []) ctx
-  in ctx, b', Array.of_list args
+  let rec aux ctx c ty =
+    match kind_of_term c, kind_of_term ty with
+    | LetIn (x, b, t, c), LetIn (x', b', t', ty)
+	 when eq_constr b b' && eq_constr t t' ->
+       let ctx' = Context.Rel.add (LocalDef (x,b',t')) ctx in
+       aux ctx' c ty
+    | _, LetIn (x', b', t', ty) ->
+       let ctx' = Context.Rel.add (LocalDef (x',b',t')) ctx in
+       aux ctx' (lift 1 c) ty
+    | LetIn (x, b, t, c), _ ->
+       let ctx' = Context.Rel.add (LocalDef (x,b,t)) ctx in
+       aux ctx' c (lift 1 ty)
+    | Lambda (x, b, t), Prod (x', b', t')
+       (* By invariant, must be convertible *) ->
+       let ctx' = Context.Rel.add (LocalAssum (x,b')) ctx in
+       aux ctx' t t'
+    | Cast (c, _, _), _ -> aux ctx c ty
+    | _, _ -> ctx, c, ty
+  in aux Context.Rel.empty c ty
+
+let shrink_body c ty =
+  let open Context.Rel.Declaration in
+  let ctx, b, ty =
+    match ty with
+    | None ->
+       let ctx, b = decompose_lam_assum c in
+       ctx, b, None
+    | Some ty ->
+       let ctx, b, ty = decompose_lam_prod c ty in
+       ctx, b, Some ty
+  in
+  let b', ty', n, args =
+    List.fold_left (fun (b, ty, i, args) decl ->
+        if noccurn 1 b && Option.cata (noccurn 1) true ty then
+	  subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args
+	else
+	  let args = if is_local_assum decl then mkRel i :: args else args in
+          mkLambda_or_LetIn decl b, Option.map (mkProd_or_LetIn decl) ty,
+	  succ i, args)
+     (b, ty, 1, []) ctx
+  in ctx, b', ty', Array.of_list args
 
 let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
 
@@ -601,15 +632,15 @@ let declare_obligation prg obl body ty uctx =
   | force, Evar_kinds.Define opaque ->
       let opaque = not force && opaque in
       let poly = pi2 prg.prg_kind in
-      let ctx, body, args =
+      let ctx, body, ty, args =
 	if get_shrink_obligations () && not poly then
-	  shrink_body body else [], body, [||]
+	  shrink_body body ty else [], body, ty, [||]
       in
       let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
       let ce =
         { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
           const_entry_secctx = None;
-	  const_entry_type = if List.is_empty ctx then ty else None;
+	  const_entry_type = ty;
 	  const_entry_polymorphic = poly;
 	  const_entry_universes = uctx;
 	  const_entry_opaque = opaque;
-- 
cgit v1.2.3


From 5193311836394d3d18a0187a0d77657aa060b651 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 21 Jun 2016 19:06:30 +0200
Subject: Update CHANGES and COMPATIBILITY

---
 CHANGES       |  9 +++++++--
 COMPATIBILITY | 14 ++++++++++++++
 2 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/CHANGES b/CHANGES
index 0f0a7a04bb..63619a55b8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,6 +15,8 @@ Tactics
 - Flag "Bracketing Last Introduction Pattern" is now on by default.
 - New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
   tactical w.r.t. variables appearing in the body of the proof.
+  On by default and deprecated. Minor source of incompatibility
+  for code relying on the precise arguments of abstracted proofs.
 - Serious bugs are fixed in tactic "double induction" (source of
   incompatibilities as soon as the inductive types have dependencies in
   the type of their constructors; "double induction" remains however
@@ -48,8 +50,11 @@ Hints
 
 Program
 
-- The "Shrink Obligations" flag now applies to all obligations, not only those
-  solved by the automatic tactic.
+- The "Shrink Obligations" flag now applies to all obligations, not only
+  those solved by the automatic tactic.
+- "Shrink Obligations" is on by default and deprecated. Minor source of
+  incompatibility for code relying on the precise arguments of
+  obligations.
 
 Notations
 
diff --git a/COMPATIBILITY b/COMPATIBILITY
index 883b8576d2..892eaa599e 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -1,3 +1,17 @@
+Potential sources of incompatibilities between Coq V8.5 and V8.6
+----------------------------------------------------------------
+
+Symptom: An obligation generated by Program or an abstracted subproof
+has different arguments.
+Cause: Set Shrink Abstract and Set Shrink Obligations are on by default
+and the subproof does not use the argument.
+Remedy:
+- Adapt the script.
+- Write an explicit lemma to prove the obligation/subproof and use it
+  instead (compatible with 8.4).
+- Unset the option for the program/proof the obligation/subproof originates
+  from.
+  
 Potential sources of incompatibilities between Coq V8.4 and V8.5
 ----------------------------------------------------------------
 
-- 
cgit v1.2.3