Fix some bugs, add possibility of automatically solving a proof statement's obligations and start the proof afterwards. Changes the architecture of subtac_obligations a bit.

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

11 files changed, 134 insertions, 86 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 2a84fdd003..a3d95ab62d 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -17,12 +17,16 @@ let trace s =
   if !Options.debug then (msgnl s; msgerr s)
   else ()
 
+let succfix (depth, fixrels) = 
+  (succ depth, List.map succ fixrels)
+
 (** 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 c = match kind_of_term c with
+  let rec substrec (depth, fixrels) c = match kind_of_term c with
     | Evar (k, args) ->
 	let (id, idstr), hyps, chop, _, _ = 
 	  try evar_info k
@@ -42,7 +46,7 @@ let subst_evar_constr evs n t =
 	  let rec aux hyps args acc =
 	     match hyps, args with
 		 ((_, None, _) :: tlh), (c :: tla) -> 
-		   aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc)
+		   aux tlh tla ((map_constr_with_binders succfix substrec (depth, fixrels) c) :: acc)
 	       | ((_, Some _, _) :: tlh), (_ :: tla) ->
 		   aux tlh tla acc
 	       | [], [] -> acc
@@ -53,11 +57,15 @@ let subst_evar_constr evs n t =
 			int (List.length hyps) ++ str " hypotheses" ++ spc () ++
 			pp_list (fun x -> my_print_constr (Global.env ()) x) args);
  	   with _ -> ());
+	  if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then
+	    transparent := Idset.add idstr !transparent;
 	  mkApp (mkVar idstr, Array.of_list args)
-    | _ -> map_constr_with_binders succ substrec depth c
+    | Fix _ ->
+	map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c
+    | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c
   in 
-  let t' = substrec 0 t in
-    t', !seen
+  let t' = substrec (0, []) t in
+    t', !seen, !transparent
 
       
 (** Substitute variable references in t using De Bruijn indices, 
@@ -74,26 +82,29 @@ let subst_vars acc n t =
     to a product : forall H1 : t1, ..., forall Hn : tn, concl.
     Changes evars and hypothesis references to variable references.
     A little optimization: don't include unnecessary let-ins and their dependencies.
-*)
+*) 
 let etype_of_evar evs hyps concl =
   let rec aux acc n = function
       (id, copt, t) :: tl ->
-	let t', s = subst_evar_constr evs n t in
+	let t', s, trans = subst_evar_constr evs n t in
 	let t'' = subst_vars acc 0 t' in
-	let rest, s' = aux (id :: acc) (succ n) tl in
+	let rest, s', trans' = aux (id :: acc) (succ n) tl in
 	let s' = Intset.union s s' in
+	let trans' = Idset.union trans trans' in
 	  (match copt with
 	      Some c -> 
-		if noccurn 1 rest then lift (-1) rest, s'
+		if noccurn 1 rest then lift (-1) rest, s', trans'
 		else
-		  let c', s'' = subst_evar_constr evs n c in
+		  let c', s'', trans'' = subst_evar_constr evs n c in
 		  let c' = subst_vars acc 0 c' in
-		    mkNamedProd_or_LetIn (id, Some c', t'') rest, Intset.union s'' s'
+		    mkNamedProd_or_LetIn (id, Some c', t'') rest, 
+		Intset.union s'' s', 
+		Idset.union trans'' trans'
 	    | None -> 
-		mkNamedProd_or_LetIn (id, None, t'') rest, s')
+		mkNamedProd_or_LetIn (id, None, t'') rest, s', trans')
     | [] ->
-	let t', s = subst_evar_constr evs n concl in
-	  subst_vars acc 0 t', s
+	let t', s, trans = subst_evar_constr evs n concl in
+	  subst_vars acc 0 t', s, trans
   in aux [] 0 (rev hyps)
 
 
@@ -110,12 +121,14 @@ 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 name nclen isevars evm fs t tycon = 
+let eterm_obligations env name isevars evm fs t tycon = 
   (* 'Serialize' the evars, we assume that the types of the existentials
      refer to previous existentials in the list only *)
   trace (str " In eterm: isevars: " ++ my_print_evardefs isevars);
   trace (str "Term given to eterm" ++ spc () ++
 	    Termops.print_constr_env (Global.env ()) t);
+  let nc = Environ.named_context env in
+  let nc_len = Sign.named_context_length nc in
   let evl = List.rev (to_list evm) in
   let evn = 
     let i = ref (-1) in
@@ -129,8 +142,8 @@ let eterm_obligations name nclen isevars evm fs t tycon =
     fold_right 
       (fun (id, (n, nstr), ev) l ->
 	 let hyps = Environ.named_context_of_val ev.evar_hyps in
-	 let hyps = trunc_named_context nclen hyps in
-	 let evtyp, deps = etype_of_evar l hyps ev.evar_concl in
+	 let hyps = trunc_named_context nc_len hyps in
+	 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 -> 
@@ -149,11 +162,11 @@ let eterm_obligations name nclen isevars evm fs t tycon =
 	   y' :: l) 
       evn []
   in 
-  let t', _ = (* Substitute evar refs in the term by variables *)
+  let t', _, transparent = (* Substitute evar refs in the term by variables *)
     subst_evar_constr evts 0 t 
   in
   let evars = 
-    List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None), deps) evts
+    List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None) && not (Idset.mem name transparent), deps) evts
   in
     (try
        trace (str "Term constructed in eterm" ++ spc () ++
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index 71fd766e35..a2582c5ca0 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 (*i $Id$ i*)
-
+open Environ
 open Tacmach
 open Term
 open Evd
@@ -18,9 +18,9 @@ val mkMetas : int -> constr list
 
 (* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *)
 
-(* id, named context length, evars, number of
+(* env, id, evars, number of
    function prototypes to try to clear from evars contexts, object and optional type *)
-val eterm_obligations : identifier -> int -> evar_defs -> evar_map -> int -> constr -> types option -> 
+val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types option -> 
   (identifier * types * bool * Intset.t) array * constr
     (* Obl. name, type as product, opacity (true = opaque) and dependencies as indexes into the array *)
 
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 1d10405c9d..56398a9fa6 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -63,8 +63,18 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
   let evm, c, typ = 
     Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None 
   in
-  let _ = Typeops.infer_type env c in
-    Command.start_proof id kind c hook
+    if not (evm = Evd.empty) then 
+      let stmt_id = Nameops.add_suffix id "_stmt" in
+      let obls, c' = eterm_obligations env stmt_id !isevars evm 0 c (Some typ) in
+	match Subtac_obligations.add_definition stmt_id c' typ obls with
+	    Subtac_obligations.Defined cst -> Command.start_proof id kind (constant_value (Global.env()) cst) hook
+	  | _ -> 
+	      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
+	Command.start_proof id kind c hook
       
 let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
 
@@ -104,9 +114,9 @@ let subtac (loc, command) =
   match command with
 	VernacDefinition (defkind, (locid, id), expr, hook) -> 
 	    (match expr with
-		 ProveBody (bl, c) -> Subtac_pretyping.subtac_proof env isevars id bl c None
-	       | DefineBody (bl, _, c, tycon) -> 
-		   Subtac_pretyping.subtac_proof env isevars id bl c tycon)
+		 ProveBody (bl, c) -> ignore(Subtac_pretyping.subtac_proof env isevars id bl c None)
+	       | DefineBody (cbl, bl, _, c, tycon) -> 
+		   ignore(Subtac_pretyping.subtac_proof env isevars id bl c tycon))
       | VernacFixpoint (l, b) -> 
 	  let _ = trace (str "Building fixpoint") in
 	    ignore(Subtac_command.build_recursive l b)
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 743d239881..1fb079fac6 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -132,6 +132,10 @@ module Coercion = struct
       let rec coerce_application typ c c' l l' =
 	let len = Array.length l in
 	let rec aux tele typ i co = 
+(* 	  (try trace (str "coerce_application.aux from " ++ (my_print_constr env x) ++ *)
+(* 			 str " to "++ my_print_constr env y *)
+(* 		       ++ str "in env:" ++ my_print_env env); *)
+(* 	    with _ -> ()); *)
 	  if i < len then
 	    let hdx = l.(i) and hdy = l'.(i) in
 	      try isevars := the_conv_x_leq env hdx hdy !isevars;
@@ -149,14 +153,15 @@ module Coercion = struct
 		let evar = make_existential dummy_loc env isevars eq in
 		let eq_app x = mkApp (Lazy.force eq_rect,
 				      [| eqT; hdx; pred; x; hdy; evar|]) in
-		  trace (str"Inserting coercion at application");
+(* 		  trace (str"Inserting coercion at application"); *)
 		  aux (hdy :: tele) (subst1 hdy restT) (succ i)  (fun x -> eq_app (co x))
 	  else co
 	in aux [] typ 0 (fun x -> x)
       in
-(* 	(try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++  *)
-(* 		    str " to "++ my_print_constr env y); *)
-(* 	 with _ -> ()); *)
+(* 	(try trace (str "coerce' from " ++ (my_print_constr env x) ++ *)
+(* 		       str " to "++ my_print_constr env y *)
+(* 		       ++ str "in env:" ++ my_print_env env); *)
+(* 	  with _ -> ()); *)
 	match (kind_of_term x, kind_of_term y) with
 	  | Sort s, Sort s' -> 
 	      (match s, s' with
@@ -167,6 +172,7 @@ module Coercion = struct
 	  | Prod (name, a, b), Prod (name', a', b') ->
 	      let name' = Name (Nameops.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in
 	      let env' = push_rel (name', None, a') env in
+		
 	      let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
 	      let c2 = coerce_unify env' b b' in
 		(match c1, c2 with
@@ -181,10 +187,11 @@ module Coercion = struct
 		  
 	  | App (c, l), App (c', l') ->
 	      (match kind_of_term c, kind_of_term c' with
-		   Ind i, Ind i' -> (* Sigma types *)
+		   Ind i, Ind i' -> (* Inductive types *)
 		     let len = Array.length l in
 		     let existS = Lazy.force existS in
 		     let prod = Lazy.force prod in
+		       (* Sigma types *)
 		       if len = Array.length l' && len = 2 && i = i'
 			 && (i = Term.destInd existS.typ || i = Term.destInd prod.typ)
 		       then 
@@ -508,9 +515,9 @@ module Coercion = struct
 	  (isevars, cj)
 
   let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) =
-(*     (try  *)
+(*     (try *)
 (*        trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++ *)
-(* 	      Termops.print_constr_env env t ++ str " and "++ spc () ++  *)
+(* 	      Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
 (* 	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *)
 (* 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
 (* 	      Termops.print_env env); *)
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 25b1627d65..9cbfb02464 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -175,8 +175,6 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let sigma = Evd.empty in
   let isevars = ref (Evd.create_evar_defs sigma) in
   let env = Global.env() in 
-  let nc = named_context env in
-  let nc_len = named_context_length nc in
   let pr c = my_print_constr env c in
   let prr = Printer.pr_rel_context env in
   let _prn = Printer.pr_named_context env in
@@ -318,7 +316,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let evm = non_instanciated_map env isevars evm in
 
     (*   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in *)
-  let evars, evars_def = Eterm.eterm_obligations recname nc_len !isevars evm 0 fullcoqc (Some fullctyp) in
+  let evars, evars_def = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc (Some fullctyp) in
     (*     (try trace (str "Generated obligations : "); *)
 (*        Array.iter *)
     (* 	 (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *)
@@ -332,8 +330,6 @@ let nf_evar_context isevars ctx =
     
 let build_mutrec lnameargsardef boxed = 
   let sigma = Evd.empty and env = Global.env () in 
-  let nc = named_context env in
-  let nc_len = named_context_length nc in
   let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef 
   and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
   in
@@ -420,7 +416,7 @@ let build_mutrec lnameargsardef boxed =
 	Termops.it_mkNamedProd_or_LetIn typ rec_sign
       in
       let evm = Subtac_utils.evars_of_term evm Evd.empty def in
-      let evars, def = Eterm.eterm_obligations id nc_len isevars evm recdefs def (Some typ) in
+      let evars, def = Eterm.eterm_obligations env id isevars evm recdefs def (Some typ) in
 	collect_evars (succ i) ((id, def, typ, evars) :: acc)
     else acc
   in 
@@ -435,9 +431,9 @@ let out_n = function
 let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
   match lnameargsardef with
     | ((id, (n, CWfRec r), bl, typ, body), no) :: [] -> 
-	build_wellfounded (id, out_n n, bl, typ, body) r false no boxed
+	ignore(build_wellfounded (id, out_n n, bl, typ, body) r false no boxed)
     | ((id, (n, CMeasureRec r), bl, typ, body), no) :: [] -> 
-	build_wellfounded (id, out_n n, bl, typ, body) r true no boxed
+	ignore(build_wellfounded (id, out_n n, bl, typ, body) r true no boxed)
     | l -> 
 	let lnameargsardef = 
 	  List.map (fun ((id, (n, ro), bl, typ, body), no) ->
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 76f79443e1..941a7576e8 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -1,4 +1,3 @@
-(* -*- default-directory: "~/research/coq/trunk/" -*- *)
 open Printf
 open Pp
 open Subtac_utils
@@ -140,10 +139,11 @@ let declare_definition prg =
       const_entry_opaque = false;
       const_entry_boxed = false} 
   in
-  let _constant = Declare.declare_constant 
+  let c = Declare.declare_constant 
     prg.prg_name (DefinitionEntry ce,IsDefinition Definition)
   in
-    Subtac_utils.definition_message prg.prg_name
+    print_message (definition_message c);
+    c
 
 open Pp
 open Ppconstr
@@ -171,12 +171,11 @@ let declare_mutual_definition l =
         const_entry_type = Some arrec.(i);
         const_entry_opaque = false;
         const_entry_boxed = true} in
-    let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
-    in
-      ConstRef kn
+      Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
   in
   let lrefrec = Array.mapi declare namerec in
-    Options.if_verbose ppnl (recursive_message lrefrec)
+    print_message (recursive_message lrefrec);
+    lrefrec.(0)    
          
 let declare_obligation obl body =
   let ce = 
@@ -188,7 +187,7 @@ let declare_obligation obl body =
   let constant = Declare.declare_constant obl.obl_name 
     (DefinitionEntry ce,IsProof Property)
   in
-    Subtac_utils.definition_message obl.obl_name;
+    print_message (definition_message constant);
     { obl with obl_body = Some (mkConst constant) }
       
 let try_tactics obls = 
@@ -241,7 +240,12 @@ let update_state s =
 (*   msgnl (str "Updating obligations info"); *)
   Lib.add_anonymous_leaf (input s)
 
-let obligations_message rem = 
+type progress = 
+    | Remain of int 
+    | Dependent
+    | Defined of constant
+	  
+let obligations_message rem =
   if rem > 0 then
     if rem = 1 then
       Options.if_verbose msgnl (int rem ++ str " obligation remaining")
@@ -249,26 +253,31 @@ let obligations_message rem =
       Options.if_verbose msgnl (int rem ++ str " obligations remaining")
   else
     Options.if_verbose msgnl (str "No more obligations remaining")
-      
+
 let update_obls prg obls rem = 
   let prg' = { prg with prg_obligations = (obls, rem) } in
     from_prg := map_replace prg.prg_name prg' !from_prg;
     obligations_message rem;
-    if rem > 0 then ()
-    else (
-      match prg'.prg_deps with
-	  [] ->
-	    declare_definition prg';
-	    from_prg := ProgMap.remove prg.prg_name !from_prg
-	| l ->
-	    let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
-	      if List.for_all (fun x -> obligations_solved x) progs then 
-		(declare_mutual_definition progs;
-		 from_prg := List.fold_left
-		   (fun acc x -> 
-		     ProgMap.remove x.prg_name acc) !from_prg progs));
-    update_state (!from_prg, !default_tactic_expr);
-    rem
+    let res = 
+      if rem > 0 then Remain rem
+      else (
+	match prg'.prg_deps with
+	    [] ->
+	      let kn = declare_definition prg' in
+		from_prg := ProgMap.remove prg.prg_name !from_prg;
+		Defined kn
+	  | l ->
+	      let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
+		if List.for_all (fun x -> obligations_solved x) progs then 
+		  (let kn = declare_mutual_definition progs in
+		     from_prg := List.fold_left
+		       (fun acc x -> 
+			 ProgMap.remove x.prg_name acc) !from_prg progs;
+		    Defined kn)
+		else Dependent);
+    in
+      update_state (!from_prg, !default_tactic_expr);
+      res
 	    
 let is_defined obls x = obls.(x).obl_body <> None
 
@@ -312,8 +321,10 @@ let rec solve_obligation prg num =
 		   let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
 		   let obls = Array.copy obls in
 		   let _ = obls.(num) <- obl in
-		     if update_obls prg obls (pred rem) <> 0 then
-		       auto_solve_obligations (Some prg.prg_name));
+		     match update_obls prg obls (pred rem) with
+			 Remain n when n > 0 ->
+			   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
@@ -378,9 +389,9 @@ and try_solve_obligation n prg tac =
 and try_solve_obligations n tac = 
   try ignore (solve_obligations n tac) with NoObligations _ -> ()
 
-and auto_solve_obligations n : unit =
+and auto_solve_obligations n : progress =
   Options.if_verbose msgnl (str "Solving obligations automatically...");
-  try_solve_obligations n !default_tactic
+  try solve_obligations n !default_tactic with NoObligations _ -> Dependent
       
 let add_definition n b t obls =
   Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
@@ -388,8 +399,9 @@ let add_definition n b t obls =
   let obls,_ = prg.prg_obligations in
   if Array.length obls = 0 then (
     Options.if_verbose ppnl (str ".");    
-    declare_definition prg;
-    from_prg := ProgMap.remove prg.prg_name !from_prg)
+    let cst = declare_definition prg in 
+      from_prg := ProgMap.remove prg.prg_name !from_prg;
+      Defined cst)
   else (
     let len = Array.length obls in
     let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
@@ -405,7 +417,7 @@ let add_mutual_definitions l nvrec =
       !from_prg l
   in
     from_prg := upd;
-    List.iter (fun x -> auto_solve_obligations (Some x)) deps
+    List.iter (fun x -> ignore(auto_solve_obligations (Some x))) deps
 
 let admit_obligations n =
   let prg = get_prog_err n in
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index f015b80b95..cd70d5233d 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -1,13 +1,19 @@
+open Names
 open Util
 
 type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array
     (* ident, type, opaque or transparent, dependencies *)
 
+type progress = (* Resolution status of a program *)
+    | Remain of int  (* n obligations remaining *)
+    | Dependent (* Dependent on other definitions *)
+    | Defined of constant (* Defined as id *)
+	
 val set_default_tactic : Tacexpr.glob_tactic_expr -> unit
 val default_tactic : unit -> Proof_type.tactic
 
 val add_definition : Names.identifier ->  Term.constr -> Term.types -> 
-  obligation_info -> unit
+  obligation_info -> progress
 
 val add_mutual_definitions : 
   (Names.identifier * Term.constr * Term.types * obligation_info) list -> int array -> unit
@@ -16,7 +22,7 @@ val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr op
 
 val next_obligation : Names.identifier option -> unit
 
-val solve_obligations : Names.identifier option -> Proof_type.tactic -> int 
+val solve_obligations : Names.identifier option -> Proof_type.tactic -> progress
 (* Number of remaining obligations to be solved for this program *)
 
 val solve_all_obligations : Proof_type.tactic -> unit 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index c6e099ac56..a0e7e6951c 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -149,8 +149,7 @@ let subtac_process env isevars id l c tycon =
 open Subtac_obligations
 
 let subtac_proof env isevars id l c tycon =
-  let nc = named_context env in
-  let nc_len = named_context_length nc in
   let evm, coqc, coqt = subtac_process env isevars id l c tycon in
-  let evars, def = Eterm.eterm_obligations id nc_len !isevars evm 0 coqc (Some coqt) in
+  let evm = Subtac_utils.evars_of_term evm Evd.empty coqc in
+  let evars, def = Eterm.eterm_obligations env id !isevars evm 0 coqc (Some coqt) in
     add_definition id def coqt evars
diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli
index b62a8766aa..afe554c87e 100644
--- a/contrib/subtac/subtac_pretyping.mli
+++ b/contrib/subtac/subtac_pretyping.mli
@@ -12,4 +12,4 @@ val subtac_process : env -> evar_defs ref -> identifier -> local_binder list ->
   constr_expr -> constr_expr option -> evar_map * constr * types
 
 val subtac_proof : env -> evar_defs ref -> identifier -> local_binder list ->
-  constr_expr -> constr_expr option -> unit
+  constr_expr -> constr_expr option -> Subtac_obligations.progress
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 9ebb8774b4..44638f496b 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -343,15 +343,18 @@ let id_of_name = function
   | Anonymous -> raise (Invalid_argument "id_of_name")
 
 let definition_message id =
-  Options.if_verbose message ((string_of_id id) ^ " is defined")
-
+  Printer.pr_constant (Global.env ()) id ++ str " is defined"
+    
 let recursive_message v =
   match Array.length v with
     | 0 -> error "no recursive definition"
-    | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined")
-    | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
+    | 1 -> (Printer.pr_constant (Global.env ()) v.(0) ++ str " is recursively defined")
+    | _ -> hov 0 (prvect_with_sep pr_coma (Printer.pr_constant (Global.env ())) v ++
 		    spc () ++ str "are recursively defined")
 
+let print_message m =
+  Options.if_verbose ppnl m
+
 (* Solve an obligation using tactics, return the corresponding proof term *)
 let solve_by_tac evi t =
   debug 2 (str "Solving goal using tactics: " ++ Evd.pr_evar_info evi);
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index bbf536c41f..3551b262c8 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -115,8 +115,10 @@ val destruct_ex : constr -> constr -> constr list
 
 val id_of_name : name -> identifier
 
-val definition_message : identifier -> unit
-val recursive_message : global_reference array -> std_ppcmds
+val definition_message : constant -> std_ppcmds
+val recursive_message : constant array -> std_ppcmds
+
+val print_message : std_ppcmds -> unit
 
 val solve_by_tac : evar_info -> Tacmach.tactic -> constr