Merge branch 'shrinkobl' into trunk

12 files changed, 215 insertions, 127 deletions

diff --git a/CHANGES b/CHANGES
index 0f0a7a04b..63619a55b 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 883b8576d..892eaa599 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
 ----------------------------------------------------------------
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 32267f6c4..60a3c7715 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/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/tactics/tactics.ml b/tactics/tactics.ml
index e26450531..f3e117f8c 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 0b63d7b56..25d1b192e 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/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index d6d370cb5..1e30ab919 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
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index ccc8e2ffe..bea96d0b7 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;
@@ -353,7 +342,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 +350,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 +358,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 && snd 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 =
@@ -587,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 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 = 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 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]
 
@@ -609,47 +628,47 @@ 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 = 
+      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 = 
+      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;
           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);
 	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 ->
@@ -806,7 +825,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
@@ -817,21 +836,40 @@ let obligation_terminator name num guard hook 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);
-      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 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
       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))
@@ -841,9 +879,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
@@ -884,11 +924,13 @@ 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
-  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 +951,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 +964,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 +999,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 +1025,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 +1046,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 ++
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 *)