Better handling of the opacity of proof obligations, add the possibility of

overriding the default tactic when adding a definition.


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

14 files changed, 192 insertions, 123 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 037911a19..c2d7a59f1 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -6,6 +6,7 @@
 *)
 
 open Term
+open Sign
 open Names
 open Evd
 open List
@@ -20,15 +21,26 @@ let trace s =
 let succfix (depth, fixrels) = 
   (succ depth, List.map succ fixrels)
 
+type oblinfo =
+  { ev_name: int * identifier;
+    ev_hyps: named_context;
+    ev_status : obligation_definition_status;
+    ev_chop: int option;
+    ev_loc: Util.loc;
+    ev_typ: types;
+    ev_deps: Intset.t }
+    
 (** Substitute evar references in t using De Bruijn indices, 
   where n binders were passed through. *)
+
 let subst_evar_constr evs n t = 
   let seen = ref Intset.empty in
   let transparent = ref Idset.empty in
   let evar_info id = List.assoc id evs in
   let rec substrec (depth, fixrels) c = match kind_of_term c with
     | Evar (k, args) ->
-	let (id, idstr), hyps, chop, _, _, _ = 
+	let { ev_name = (id, idstr) ; 
+	      ev_hyps = hyps ; ev_chop = chop } =
 	  try evar_info k
 	  with Not_found -> 
 	    anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
@@ -117,7 +129,7 @@ let rec chop_product n t =
       | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
       | _ -> None
 
-let eterm_obligations env name isevars evm fs t ty = 
+let eterm_obligations env name isevars evm fs ?status t ty = 
   (* 'Serialize' the evars, we assume that the types of the existentials
      refer to previous existentials in the list only *)
   let nc = Environ.named_context env in
@@ -139,14 +151,22 @@ let eterm_obligations env name isevars evm fs t ty =
 	 let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in
 	 let evtyp, hyps, chop = 
 	   match chop_product fs evtyp with
-	   Some t -> t, trunc_named_context fs hyps, fs
-	     | None -> evtyp, hyps, 0
+	   | Some t -> t, trunc_named_context fs hyps, fs
+	   | None -> evtyp, hyps, 0
 	 in
 	 let loc, k = evar_source id isevars in
-	 let opacity = match k with QuestionMark o -> o | _ -> true in
-	 let opaque = if not opacity || chop <> fs then None else Some chop in
-	 let y' = (id, ((n, nstr), hyps, opaque, loc, evtyp, deps)) in
-	   y' :: l) 
+	 let status = match k with QuestionMark o -> Some o | _ -> status in
+	 let status, chop = match status with 
+	   | Some (Define true as stat) ->
+	       if chop <> fs then Define false, None 
+	       else stat, Some chop
+	   | Some s -> s, None
+	   | None -> Define true, None
+	 in
+	 let info = { ev_name = (n, nstr);
+		      ev_hyps = hyps; ev_status = status; ev_chop = chop;
+		      ev_loc = loc; ev_typ = evtyp ; ev_deps = deps }
+	 in (id, info) :: l) 
       evn []
   in 
   let t', _, transparent = (* Substitute evar refs in the term by variables *)
@@ -154,8 +174,14 @@ let eterm_obligations env name isevars evm fs t ty =
   in
   let ty, _, _ = subst_evar_constr evts 0 ty in
   let evars = 
-    List.map (fun (_, ((_, name), _, opaque, loc, typ, deps)) -> 
-      name, typ, loc, not (opaque = None) && not (Idset.mem name transparent), deps) evts
+    List.map (fun (_, info) ->
+      let { ev_name = (_, name); ev_status = status;
+	    ev_loc = loc; ev_typ = typ; ev_deps = deps } = info
+      in
+      let status = match status with
+	| Define true when Idset.mem name transparent -> Define false
+	| _ -> status
+      in name, typ, loc, status, deps) evts
   in Array.of_list (List.rev evars), t', ty
 
 let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index bf854abb3..e197024ff 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -16,11 +16,12 @@ open Util
 
 val mkMetas : int -> constr list
 
-(* env, id, evars, number of
-   function prototypes to try to clear from evars contexts, object and type *)
-val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types -> 
-  (identifier * types * loc * bool * Intset.t) array * constr * types
+(* env, id, evars, number of function prototypes to try to clear from
+   evars contexts, object and type *)
+val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> 
+  ?status:obligation_definition_status -> constr -> types -> 
+  (identifier * types * loc * obligation_definition_status * Intset.t) array * constr * types
     (* Obl. name, type as product, location of the original evar, 
-       opacity (true = opaque) and dependencies as indexes into the array *)
+       status and dependencies as indexes into the array *)
 
 val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index baf565ab1..acf1ae838 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -52,16 +52,14 @@ open Tacexpr
 let solve_tccs_in_type env id isevars evm c typ =
   if not (evm = Evd.empty) then 
     let stmt_id = Nameops.add_suffix id "_stmt" in
-    let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 c typ in
-    (** Make all obligations transparent so that real dependencies can be sorted out by the user *)
-    let obls = Array.map (fun (id, t, l, op, d) -> (id, t, l, false, d)) obls in
+    let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
       match Subtac_obligations.add_definition stmt_id c' typ obls with
-	  Subtac_obligations.Defined cst -> constant_value (Global.env()) 
-	    (match cst with ConstRef kn -> kn | _ -> assert false)
-	| _ -> 
-	    errorlabstrm "start_proof" 
-	      (str "The statement obligations could not be resolved automatically, " ++ spc () ++
-		  str "write a statement definition first.")
+      Subtac_obligations.Defined cst -> constant_value (Global.env()) 
+	(match cst with ConstRef kn -> kn | _ -> assert false)
+      | _ -> 
+	  errorlabstrm "start_proof" 
+	    (str "The statement obligations could not be resolved automatically, " ++ spc () ++
+		str "write a statement definition first.")
   else
     let _ = Typeops.infer_type env c in c
 
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 009b80606..f45efe50b 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1572,7 +1572,7 @@ let mk_JMeq typ x typ' y =
   mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
 let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |])
     
-let hole = RHole (dummy_loc, Evd.QuestionMark true)
+let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
 
 let context_of_arsign l =
   let (x, _) = List.fold_right
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index a2f54b02d..503f34619 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -284,7 +284,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 	  mkApp (constr_of_global (Lazy.force fix_sub_ref), 
 		 [| argtyp ;
 		    wf_rel ;
-		    make_existential dummy_loc ~opaque:false env isevars wf_proof ;
+		    make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
 		    lift lift_cst prop ;
 		    lift lift_cst intern_body_lam |])
       | Some f ->
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 563b228d8..6d1ec5ede 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -1,7 +1,9 @@
+(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
 open Printf
 open Pp
 open Subtac_utils
 open Command
+open Environ
 
 open Term
 open Names
@@ -16,6 +18,7 @@ open Declare
 
 type definition_hook = global_reference -> unit
 
+let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
 let pperror cmd = Util.errorlabstrm "Program" cmd
 let error s = pperror (str s)
 
@@ -25,14 +28,14 @@ let explain_no_obligations = function
     Some ident -> str "No obligations for program " ++ str (string_of_id ident)
   | None -> str "No obligations remaining"
 
-type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array
+type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t) array
 
 type obligation =
     { obl_name : identifier;
       obl_type : types;
       obl_location : loc;
       obl_body : constr option;
-      obl_opaque : bool;
+      obl_status : obligation_definition_status;
       obl_deps : Intset.t;
     }
 
@@ -79,22 +82,29 @@ let _ =
 
 let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
 
-let subst_deps obls deps t =
-  Intset.fold
-    (fun x acc ->
-       let xobl = obls.(x) in
-	 debug 3 (str "Trying to get body of obligation " ++ int x);
-       let oblb = 
-	 try Option.get xobl.obl_body
-	 with _ ->
-	   debug 3 (str "Couldn't get body of obligation " ++ int x);
-	   assert(false)
-       in
-	 Term.subst1 oblb (Term.subst_var xobl.obl_name acc))
-    deps t
-
+let get_obligation_body expand obl =
+  let c = Option.get obl.obl_body in
+    if expand && obl.obl_status = Expand then 
+      match kind_of_term c with
+      | Const c -> constant_value (Global.env ()) c
+      | _ -> c
+    else c
+
+let subst_deps expand obls deps t =
+  let subst =
+    Intset.fold
+      (fun x acc ->
+	let xobl = obls.(x) in
+	let oblb = 
+	  try get_obligation_body expand xobl
+	  with _ -> assert(false)
+	in (xobl.obl_name, oblb) :: acc)
+      deps []
+  in(*  Termops.it_mkNamedProd_or_LetIn t subst *)
+    Term.replace_vars subst t
+    
 let subst_deps_obl obls obl =
-  let t' = subst_deps obls obl.obl_deps obl.obl_type in
+  let t' = subst_deps false obls obl.obl_deps obl.obl_type in
     { obl with obl_type = t' }
 
 module ProgMap = Map.Make(struct type t = identifier let compare = compare end)
@@ -150,14 +160,14 @@ let rec intset_to = function
     -1 -> Intset.empty
   | n -> Intset.add n (intset_to (pred n))
   
-let subst_body prg = 
+let subst_body expand prg = 
   let obls, _ = prg.prg_obligations in
   let ints = intset_to (pred (Array.length obls)) in
-    subst_deps obls ints prg.prg_body,
-  subst_deps obls ints (Termops.refresh_universes prg.prg_type)
+    subst_deps expand obls ints prg.prg_body,
+  subst_deps expand obls ints (Termops.refresh_universes prg.prg_type)
     
 let declare_definition prg =
-  let body, typ = subst_body prg in
+  let body, typ = subst_body false prg in
     (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
 		  my_print_constr (Global.env()) body ++ str " : " ++ 
 		  my_print_constr (Global.env()) prg.prg_type);
@@ -216,14 +226,18 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
       let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
 	list_map_i (fun i _ -> i) 0 ctx
 
+let reduce_fix =
+  Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty
+
 let declare_mutual_definition l =
   let len = List.length l in
   let fixdefs, fixtypes, fiximps = 
     list_split3
       (List.map (fun x -> 
-	let subs, typ = (subst_body x) in
+	let subs, typ = (subst_body false x) in
 	  snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
   in
+(*   let fixdefs = List.map reduce_fix fixdefs in *)
   let fixkind = Option.get (List.hd l).prg_fixkind in
   let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
   let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
@@ -248,18 +262,23 @@ let declare_mutual_definition l =
     (match List.hd kns with ConstRef kn -> kn | _ -> assert false)
       
 let declare_obligation obl body =
-  let ce = 
-    { const_entry_body = body;
-      const_entry_type = Some obl.obl_type;
-      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 
-    (DefinitionEntry ce,IsProof Property)
-  in
-    print_message (Subtac_utils.definition_message obl.obl_name);
-    { obl with obl_body = Some (mkConst constant) }
-      
+  match obl.obl_status with
+  | Expand -> { obl with obl_body = Some body }
+  | Define opaque ->
+      let ce = 
+	{ const_entry_body = body;
+	  const_entry_type = Some obl.obl_type;
+	  const_entry_opaque = 
+	    (if get_proofs_transparency () then false 
+	      else opaque) ;
+	  const_entry_boxed = false} 
+      in
+      let constant = Declare.declare_constant obl.obl_name 
+	(DefinitionEntry ce,IsProof Property)
+      in
+	print_message (Subtac_utils.definition_message obl.obl_name);
+	{ obl with obl_body = Some (mkConst constant) }
+	  
 let red = Reductionops.nf_betaiota
 
 let init_prog_info n b t deps fixkind notations obls impls kind hook =
@@ -268,7 +287,7 @@ let init_prog_info n b t deps fixkind notations obls impls kind hook =
       (fun i (n, t, l, o, d) ->
 	 debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
          { obl_name = n ; obl_body = None; 
-	   obl_location = l; obl_type = red t; obl_opaque = o;
+	   obl_location = l; obl_type = red t; obl_status = o;
 	   obl_deps = d })
       obls
   in
@@ -356,22 +375,16 @@ let has_dependencies obls n =
     !res
       
 let kind_of_opacity o =
-  if o then Subtac_utils.goal_proof_kind
-  else Subtac_utils.goal_kind
-   
-let obligations_of_evars evars =
-  let arr = 
-    Array.of_list
-      (List.map
-	 (fun (n, t) ->
-	    { obl_name = n;
-	      obl_type = t;
-	      obl_location = dummy_loc;
-	      obl_body = None;
-	      obl_opaque = false;
-	      obl_deps = Intset.empty;
-	    }) evars)
-  in arr, Array.length arr
+  match o with
+  | Define false | Expand -> Subtac_utils.goal_kind
+  | _ -> Subtac_utils.goal_proof_kind
+
+let not_transp_msg = 
+  str "Obligation should be transparent but was declared opaque." ++ spc () ++
+    str"Use 'Defined' instead."
+
+let warn_not_transp () = ppwarn not_transp_msg
+let error_not_transp () = pperror not_transp_msg
 
 let rec solve_obligation prg num =
   let user_num = succ num in
@@ -381,26 +394,37 @@ let rec solve_obligation prg num =
       pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")    
     else
       match deps_remaining obls obl.obl_deps with
-	  [] ->
-	    let obl = subst_deps_obl obls obl in
-	      Command.start_proof obl.obl_name (kind_of_opacity obl.obl_opaque) obl.obl_type
-		(fun strength gr -> 
-		   debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished");		   
-		   let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
-		   let obls = Array.copy obls in
-		   let _ = obls.(num) <- obl in
-		     match update_obls prg obls (pred rem) with
-		     | Remain n when n > 0 ->
-			 if has_dependencies obls num then
-			   ignore(auto_solve_obligations (Some prg.prg_name))
-		     | _ -> ());
-	      trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
-		       Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
-	      Pfedit.by !default_tactic;
-	      Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
-	| l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
-			++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
-
+      | [] ->
+	  let obl = subst_deps_obl obls obl in
+	    Command.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
+	      (fun strength gr -> 
+		let cst = match gr with ConstRef cst -> cst | _ -> assert false in
+		let obl = 
+		  let transparent = evaluable_constant cst (Global.env ()) in
+		  let body =
+		    match obl.obl_status with
+		    | Expand ->
+			if not transparent then error_not_transp ()
+			else constant_value (Global.env ()) cst
+		    | Define opaque ->
+			if not opaque && not transparent then error_not_transp ()
+			else Libnames.constr_of_global gr
+		  in { obl with obl_body = Some body }
+		in
+		let obls = Array.copy obls in
+		let _ = obls.(num) <- obl in
+		  match update_obls prg obls (pred rem) with
+		  | Remain n when n > 0 ->
+		      if has_dependencies obls num then
+			ignore(auto_solve_obligations (Some prg.prg_name))
+		  | _ -> ());
+	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
+		      Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
+	    Pfedit.by !default_tactic;
+	    Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
+      | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
+		       ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
+	  
 and subtac_obligation (user_num, name, typ) =
   let num = pred user_num in
   let prg = get_prog_err name in
@@ -422,11 +446,8 @@ and solve_obligation_by_tac prg obls i tac =
 	    if deps_remaining obls obl.obl_deps = [] then
 	     let obl = subst_deps_obl obls obl in
 	     let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
-	       if obl.obl_opaque then 
-		 obls.(i) <- declare_obligation obl t
-	       else
-		 obls.(i) <- { obl with obl_body = Some t };
-	       true		 
+	       obls.(i) <- declare_obligation obl t;
+	       true
 	    else false
 	  with
 	    | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
@@ -473,21 +494,25 @@ let show_obligations ?(msg=true) n =
   let prg = get_prog_err n in
   let n = prg.prg_name in
   let obls, rem = prg.prg_obligations in
+  let showed = ref 5 in
     if msg then msgnl (int rem ++ str " obligation(s) remaining: ");
     Array.iteri (fun i x -> 
 		   match x.obl_body with 
-		       None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ 
-					my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())
-		    | Some _ -> ())
+		   | None -> 
+		       if !showed > 0 then (
+			 decr showed;
+			 msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ 
+				   hov 1 (my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())))
+		   | Some _ -> ())
       obls
-
+      
 let show_term n =
   let prg = get_prog_err n in
   let n = prg.prg_name in
     msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ my_print_constr (Global.env ()) prg.prg_body)
 
-let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?(hook=fun x -> ()) obls =
+let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun x -> ()) obls =
   Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
   let prg = init_prog_info n b t [] None [] obls implicits kind hook in
   let obls,_ = prg.prg_obligations in
@@ -500,12 +525,16 @@ let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?(hook=
     let len = Array.length obls in
     let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
       from_prg := ProgMap.add n prg !from_prg; 
-      let res = auto_solve_obligations (Some n) in
+      let res =
+	match tactic with
+	| None -> auto_solve_obligations (Some n) 
+	| Some tac -> solve_obligations (Some n) tac
+      in
 	match res with
-	  | Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
-	  | _ -> res)
+	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
+	| _ -> res)
 	
-let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind =
+let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
   let upd = List.fold_left
       (fun acc (n, b, t, imps, obls) ->
@@ -518,8 +547,13 @@ let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind =
       List.fold_left (fun finished x -> 
 	if finished then finished 
 	else
-	  match auto_solve_obligations (Some x) with
-	      Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true
+	  let res =
+	    match tactic with
+	    | None -> auto_solve_obligations (Some x) 
+	    | Some tac -> solve_obligations (Some x) tac
+	  in
+	    match res with
+	    | Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true
 	    | _ -> false) 
 	false deps
     in ()
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 6d13e3bd3..355ca7cd7 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -1,9 +1,10 @@
 open Names
 open Util
 open Libnames
+open Evd
 
-type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array
-    (* ident, type, location, opaque or transparent, dependencies *)
+type obligation_info = (identifier * Term.types * loc * obligation_definition_status * Intset.t) array
+    (* ident, type, location, opaque or transparent, expand or define dependencies *)
 
 type progress = (* Resolution status of a program *)
     | Remain of int  (* n obligations remaining *)
@@ -21,6 +22,7 @@ type definition_hook = global_reference -> unit
 val add_definition : Names.identifier ->  Term.constr -> Term.types -> 
   ?implicits:(Topconstr.explicitation * (bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
+  ?tactic:Proof_type.tactic ->
   ?hook:definition_hook -> obligation_info -> progress
 
 type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
@@ -28,6 +30,7 @@ type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option)
 val add_mutual_definitions : 
   (Names.identifier * Term.constr * Term.types *
       (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> 
+  ?tactic:Proof_type.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   notations ->
   Command.fixpoint_kind -> unit
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index bae2731aa..920b33b7a 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -159,7 +159,7 @@ let app_opt c e =
 let print_args env args = 
   Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "")
 
-let make_existential loc ?(opaque = true) env isevars c =
+let make_existential loc ?(opaque = Define true) env isevars c =
   let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in
   let (key, args) = destEvar evar in
     (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++
@@ -470,4 +470,3 @@ let tactics_tac s =
 
 let tactics_call tac args =
   TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args))
-
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 493352114..964f668f2 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -83,7 +83,8 @@ val wf_relations : (constr, constr lazy_t) Hashtbl.t
 type binders = local_binder list
 val app_opt : ('a -> 'a) option -> 'a -> 'a
 val print_args : env -> constr array -> std_ppcmds
-val make_existential : loc -> ?opaque:bool -> env -> evar_defs ref -> types -> constr
+val make_existential : loc -> ?opaque:obligation_definition_status -> 
+  env -> evar_defs ref -> types -> constr
 val make_existential_expr : loc -> 'a -> 'b -> constr_expr
 val string_of_hole_kind : hole_kind -> string
 val evars_of_term : evar_map -> evar_map -> constr -> evar_map
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 26ed02379..be7c75663 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -940,7 +940,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let p' = Option.map (intern_type env'') po in
         RIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole (loc, k) -> 
-	RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark true)
+	RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
     | CPatVar (loc, n) when allow_patvar ->
 	RPatVar (loc, n)
     | CPatVar (loc, _) ->
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index 44ca8eb2c..a796cef82 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -75,7 +75,7 @@ EXTEND
     | "0"
       [ s = sort -> <:expr< Rawterm.RSort ($dloc$,s) >>
       | id = ident -> <:expr< Rawterm.RVar ($dloc$,$id$) >>
-      | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark False) >>
+      | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark (Define False)) >>
       | "?"; id = ident -> <:expr< Rawterm.RPatVar($dloc$,(False,$id$)) >>
       | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" ->
           apply_ref <:expr< coq_sumbool_ref >> [c1;c2]
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 270dac01a..b29afc0cb 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -400,10 +400,12 @@ let metamap_to_list m =
 (*************************)
 (* Unification state *)
 
+type obligation_definition_status = Define of bool | Expand
+
 type hole_kind =
   | ImplicitArg of global_reference * (int * identifier option)
   | BinderType of name
-  | QuestionMark of bool
+  | QuestionMark of obligation_definition_status
   | CasesType
   | InternalHole
   | TomatchTypeParameter of inductive * int
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index cb7429002..38db90dad 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -166,11 +166,16 @@ val empty_evar_defs : evar_defs
 val evars_of         : evar_defs -> evar_map
 val evars_reset_evd  : evar_map ->  evar_defs -> evar_defs
 
+(* Should the obligation be defined (opaque or transparent (default)) or
+   defined transparent and expanded in the term? *)
+
+type obligation_definition_status = Define of bool | Expand
+
 (* Evars *)
 type hole_kind =
   | ImplicitArg of global_reference * (int * identifier option)
   | BinderType of name
-  | QuestionMark of bool (* Can it be turned into an obligation ? *)
+  | QuestionMark of obligation_definition_status
   | CasesType
   | InternalHole
   | TomatchTypeParameter of inductive * int
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index a25fcd923..2be95056e 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -342,7 +342,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	(fun (loc,(id,_)) -> 
 	   RVar (loc,id)) params in 
     let dum_args= 
-      list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark false))
+      list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark (Evd.Define false)))
 	oib.Declarations.mind_nrealargs in
       raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in
   let pat_vars,aliases,patt = interp_pattern env pat in