Postpone the search for the recursive argument index from the user given

name after internalisation, to get the correct behavior with typeclass
binders. This simplifies the pretty printing and translation
of the recursive argument name in various places too. Use this
opportunity to factorize the different internalization and
interpretation functions of binders as well.
This definitely fixes part 2 of bug
#1846 and makes it possible to use fixpoint definitions with typeclass arguments in
program too, with an example given in EquivDec. 
At the same time, one fix and one enhancement in Program:
- fix a de Bruijn bug in subtac_cases
- introduce locations of obligations and use them in case the obligation tactic
raises a failure when tried on a particular obligation, as suggested by
Sean Wilson.


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

11 files changed, 84 insertions, 111 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 4f78c8c59c..fa49d4aa86 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -510,13 +510,8 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
 	    List.map
 	      (function
 		 | (name,Some (Struct id),args,types,body),_ -> 
-		     let names = 
-		       List.map
-			 snd
-			 (Topconstr.names_of_local_assums args) 
-		     in 
 		     let annot = 
-		       try Some (list_index0 (Name id) names), Topconstr.CStructRec 
+		       try Some (dummy_loc, id), Topconstr.CStructRec 
 		       with Not_found -> 
 			 raise (UserError("",str "Cannot find argument " ++ 
 					    Ppconstr.pr_id id)) 
@@ -529,7 +524,8 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
 			 (dummy_loc,"Function",
 			  Pp.str "the recursive argument needs to be specified in Function")
 		     else 
-		       (name,(Some 0, Topconstr.CStructRec),args,types,body),
+		       let loc, na = List.hd names in
+			 (name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body),
 		     (None:Vernacexpr.decl_notation)
 		 | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> 
 		     error 
@@ -713,20 +709,7 @@ let make_graph (f_ref:global_reference) =
 		let l = 
 		  List.map
 		    (fun (id,(n,recexp),bl,t,b) -> 
-		       let bl' =  
-			 List.flatten 
-			   (List.map 
-			      (function 
-				 | Topconstr.LocalRawDef (na,_)-> []
-				 | Topconstr.LocalRawAssum (nal,_,_) -> nal
-			      )
-			      bl
-			   )
-		       in 
-		       let rec_id = 
-			 match List.nth bl' (Option.get n)  with 
-			   |(_,Name id) -> id | _ -> anomaly ""
-		       in
+		       let loc, rec_id = Option.get n in
 		       let new_args = 
 			 List.flatten 
 			   (List.map 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 82277be4df..20bb3a4a1f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -305,11 +305,7 @@ let make_fix_struct (n,bl) =
   let names = names_of_local_assums bl in
   let nn = List.length names in
   if nn = 1 || n = None then ctv_ID_OPT_NONE
-  else 
-    let n = Option.get n in 
-    if n < nn then xlate_id_opt(List.nth names n)
-    else xlate_error "unexpected result of parsing for Fixpoint";;
-
+  else ctf_ID_OPT_SOME(CT_ident (string_of_id (snd (Option.get n))));;
 
 let rec xlate_binder = function
     (l,k,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
@@ -425,14 +421,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
    | CFix (_, (_, id), lm::lmi) ->       
      let strip_mutrec (fid, (n, ro), bl, arf, ardef) =
-        let (struct_arg,bl,arf,ardef) =
-	 (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
-	 (* By the way, how could [bl = []] happen in V8 syntax ?  *)
-         if bl = [] then
-	   let n = Option.get n in 
-           let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
-           (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
-         else (make_fix_struct (n, bl),bl,arf,ardef) in
+        let struct_arg = make_fix_struct (n, bl) in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
 	match xlate_binder_list bl with
@@ -1953,14 +1942,7 @@ let rec xlate_vernac =
    | VernacFixpoint ([],_) -> xlate_error "mutual recursive"
    | VernacFixpoint ((lm :: lmi),boxed) ->
       let strip_mutrec ((fid, (n, ro), bl, arf, ardef), _ntn) =
-        let (struct_arg,bl,arf,ardef) =
-	 (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
-	 (* By the way, how could [bl = []] happen in V8 syntax ?  *)
-         if bl = [] then
-	   let n = Option.get n in 
-           let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
-           (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
-         else (make_fix_struct (n, bl),bl,arf,ardef) in
+        let struct_arg = make_fix_struct (n, bl) in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
 	match xlate_binder_list bl with
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 8f319f9efc..9bfb33ea77 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -28,7 +28,7 @@ let subst_evar_constr evs n t =
   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 (id, idstr), hyps, chop, _, _, _ = 
 	  try evar_info k
 	  with Not_found -> 
 	    anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
@@ -158,7 +158,7 @@ let eterm_obligations env name isevars evm fs t ty =
 	 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, evtyp, deps)) in
+	 let y' = (id, ((n, nstr), hyps, opaque, loc, evtyp, deps)) in
 	   y' :: l) 
       evn []
   in 
@@ -167,13 +167,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, typ, deps)) -> name, typ, not (opaque = None) && not (Idset.mem name transparent), deps) evts
+    List.map (fun (_, ((_, name), _, opaque, loc, typ, deps)) -> 
+      name, typ, loc, not (opaque = None) && not (Idset.mem name transparent), deps) evts
   in
     (try
        trace (str "Term constructed in eterm" ++ spc () ++
 		Termops.print_constr_env (Global.env ()) t');
        ignore(iter
-		(fun (name, typ, _, deps) ->
+		(fun (name, typ, _, _, deps) ->
 		   trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++
 			    Termops.print_constr_env (Global.env ()) typ))
 		evars);
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index e23fd535ca..5f10ac1d38 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -21,7 +21,8 @@ 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 * bool * Intset.t) array * constr * types
-    (* Obl. name, type as product, opacity (true = opaque) and dependencies as indexes into the array *)
+  (identifier * types * loc * bool * 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 *)
 
 val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 9641794bea..06c67e60b1 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -54,7 +54,7 @@ let solve_tccs_in_type env id isevars evm c typ =
     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, op, d) -> (id, t, false, d)) obls in
+    let obls = Array.map (fun (id, t, l, op, d) -> (id, t, l, false, d)) obls in
       match Subtac_obligations.add_definition stmt_id c' typ obls with
 	  Subtac_obligations.Defined cst -> constant_value (Global.env()) cst
 	| _ -> 
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 6e9b741ef5..6a470afc6a 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1745,7 +1745,7 @@ let build_ineqs prevpatterns pats liftsign =
 			  len',
 			  succ n, (* nth pattern *)
 			  mkApp (Lazy.force eq_ind,
-				[| lift (succ len') curpat_ty ;
+				[| lift (len' + liftsign) curpat_ty;
 				   liftn (len + liftsign) (succ lens) ppat_c ;
 				   lift len' curpat_c |]) :: 
 			    List.map (lift lens (* Jump over this prevpat signature *)) c)
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 218c697c68..5ca313d0bb 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -150,7 +150,7 @@ module Coercion = struct
 		let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
 		let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in
 (* 		let jmeq = mkApp (Lazy.force jmeq_ind, [| eqT; hdx; eqT; hdy |]) in *)
-		let evar = make_existential dummy_loc env isevars eq in
+		let evar = make_existential 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"); *)
@@ -300,7 +300,7 @@ module Coercion = struct
 		    Some 
 		      (fun x ->
 			 let cx = app_opt c x in
-			 let evar = make_existential dummy_loc env isevars (mkApp (p, [| cx |]))
+			 let evar = make_existential loc env isevars (mkApp (p, [| cx |]))
 			 in
 			   (mkApp 
 			      ((Lazy.force sig_).intro, 
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index c29d677f55..da0e4a8e56 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -98,24 +98,30 @@ let locate_if_isevar loc na = function
 let interp_binder sigma env na t =
   let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in
     SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t)
-      
-let interp_context_evars sigma env params = 
-  List.fold_left
-    (fun (env,params) d -> match d with
-      | LocalRawAssum ([_,na],k,(CHole _ as t)) ->
-	  let t = interp_binder sigma env na t in
-	  let d = (na,None,t) in
-	  (push_rel d env, d::params)
-      | LocalRawAssum (nal,k,t) ->
-	  let t = interp_type_evars sigma env t in
-	  let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
-	  let ctx = List.rev ctx in
-	  (push_rel_context ctx env, ctx@params)
-      | LocalRawDef ((_,na),c) ->
-	  let c = interp_constr_judgment sigma env c in
-	  let d = (na, Some c.uj_val, c.uj_type) in
-	  (push_rel d env,d::params))
-    (env,[]) params
+
+let interp_context_evars evdref env params = 
+  let bl = Constrintern.intern_context (Evd.evars_of !evdref) env params in
+  let (env, par, _, impls) =
+    List.fold_left
+      (fun (env,params,n,impls) (na, k, b, t) ->
+	match b with
+	    None ->
+	      let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+	      let t = SPretyping.understand_tcc_evars evdref env IsType t' in
+	      let d = (na,None,t) in
+	      let impls = 
+		if k = Implicit then
+		  let na = match na with Name n -> Some n | Anonymous -> None in
+		    (ExplByPos (n, na), (true, true)) :: impls
+		else impls
+	      in
+		(push_rel d env, d::params, succ n, impls)
+	  | Some b ->
+	      let c = SPretyping.understand_judgment_tcc evdref env b in
+	      let d = (na, Some c.uj_val, c.uj_type) in
+		(push_rel d env,d::params, succ n, impls))
+      (env,[],1,[]) (List.rev bl)
+  in (env, par), impls
 
 (* try to find non recursive definitions *)
 
@@ -191,8 +197,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 (* 		 Ppconstr.pr_constr_expr body) *)
 (*     with _ -> () *)
     (*   in *)
-  let env', binders_rel = interp_context_evars isevars env bl in
-  let after, ((argname, _, argtyp) as arg), before = split_args (succ n) binders_rel in
+  let (env', binders_rel), impls = interp_context_evars isevars env bl in
+  let after, ((argname, _, argtyp) as arg), before = 
+    let idx = list_index (Name (snd n)) (List.rev_map (fun (na, _, _) -> na) binders_rel) in
+      split_args idx binders_rel in
   let before_length, after_length = List.length before, List.length after in
   let argid = match argname with Name n -> n | _ -> assert(false) in
   let liftafter = lift_binders 1 after_length after in
@@ -232,7 +240,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let top_env = push_rel_context top_bl env in
   let top_arity = interp_type_evars isevars top_env arityc in
   let intern_bl = wfarg 1 :: arg :: before in
-  let intern_env = push_rel_context intern_bl env in
+  let _intern_env = push_rel_context intern_bl env in
   let proj = (Lazy.force sig_).Coqlib.proj1 in
   let projection = 
     mkApp (proj, [| argtyp ;
@@ -242,32 +250,19 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 		 |])
   in
   let intern_arity = it_mkProd_or_LetIn top_arity after in
-    trace (str "After length: " ++ int after_length ++ str "Top env: " ++ prr top_bl ++ spc () ++ 
-	      str "Intern arity: " ++ my_print_constr 
-	      (push_rel_context (arg :: before) env) intern_arity);
   (* Intern arity is in top_env = arg :: before *)
   let intern_arity = liftn 2 2 intern_arity in
-    trace (str "After lifting arity: " ++ 
-	      my_print_constr (push_rel (Name argid', None, lift 2 argtyp) intern_env)
-	      intern_arity);
+(*     trace (str "After lifting arity: " ++  *)
+(* 	      my_print_constr (push_rel (Name argid', None, lift 2 argtyp) intern_env) *)
+(* 	      intern_arity); *)
   (* arity is now in something :: wfarg :: arg :: before 
      where what refered to arg now refers to something *)
   let intern_arity = substl [projection] intern_arity in
   (* substitute the projection of wfarg for something *)
-  (try trace (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ());
-(*   let intern_arity = liftn 1 (succ after_length) intern_arity in (\* back in after :: wfarg :: arg :: before (ie, jump over arg) *\) *)
-(*   (try trace (str "Top arity after subst and lift: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); *)
   let intern_before_env = push_rel_context before env in
-(*   let intern_fun_bl = liftafter @ [wfarg 1]  in (\* FixMe dependencies *\) *)
-(*   (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ()); *)
-  (try trace (str "Intern arity: " ++
-		  my_print_constr intern_env intern_arity) with _ -> ());
   let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
-  (try trace (str "Intern fun arity product: " ++
-		  my_print_constr (push_rel_context [arg] intern_before_env) intern_fun_arity_prod) with _ -> ());
   let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
   let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in
-(*   (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ()); *)
   let fun_env = push_rel_context fun_bl intern_before_env in
   let fun_arity = interp_type_evars isevars fun_env arityc in
   let intern_body = interp_casted_constr isevars fun_env body fun_arity in
@@ -338,9 +333,12 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let names = List.map (fun id -> Name id) fixnames in
   (Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
 
-let compute_possible_guardness_evidences (n,_) fixtype =
+let rel_index n ctx = 
+  list_index0 (Name n) (List.rev_map (fun (na, _, _) -> na) ctx)
+
+let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
   match n with 
-  | Some n -> [n] 
+  | Some (loc, n) -> [rel_index n fixctx] 
   | None -> 
       (* If recursive argument was not given by user, we try all args.
 	 An earlier approach was to look only for inductive arguments,
@@ -360,12 +358,7 @@ let interp_recursive fixkind l boxed =
 
   (* Interp arities allowing for unresolved types *)
   let evdref = ref (Evd.create_evar_defs Evd.empty) in
-  let fiximps = 
-    List.map 
-      (fun x -> Implicit_quantifiers.implicits_of_binders x.Command.fix_binders) 
-      fixl 
-  in
-  let fixctxs = List.map (interp_fix_context evdref env) fixl in
+  let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in
   let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let rec_sign = 
@@ -421,7 +414,7 @@ let interp_recursive fixkind l boxed =
     (match fixkind with
       | Command.IsFixpoint wfl ->
 	  let possible_indexes =
-	    List.map2 compute_possible_guardness_evidences wfl fixtypes in
+	    list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
 	  let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), 
 	    Array.of_list fixtypes, 
 	    Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
@@ -433,7 +426,7 @@ let interp_recursive fixkind l boxed =
 
 let out_n = function
     Some n -> n
-  | None -> 0
+  | None -> raise Not_found
 
 let build_recursive l b =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index c15bfb528c..bc6d5dee1a 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -24,11 +24,12 @@ 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 * bool * Intset.t) array
+type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array
 
 type obligation =
     { obl_name : identifier;
       obl_type : types;
+      obl_location : loc;
       obl_body : constr option;
       obl_opaque : bool;
       obl_deps : Intset.t;
@@ -179,9 +180,16 @@ let declare_definition prg =
 open Pp
 open Ppconstr
 
-let compute_possible_guardness_evidences (n,_) fixtype =
+let rec lam_index n t acc =
+  match kind_of_term t with
+    | Lambda (na, _, b) ->
+	if na = Name n then acc
+	else lam_index n b (succ acc)
+    | _ -> raise Not_found
+	
+let compute_possible_guardness_evidences (n,_) fixbody fixtype =
   match n with 
-  | Some n -> [n] 
+  | Some (loc, n) -> [lam_index n fixbody 0]
   | None -> 
       (* If recursive argument was not given by user, we try all args.
 	 An earlier approach was to look only for inductive arguments,
@@ -210,7 +218,7 @@ let declare_mutual_definition l =
     match fixkind with
       | IsFixpoint wfl ->
 	  let possible_indexes =
-	    List.map2 compute_possible_guardness_evidences wfl fixtypes in
+	    list_map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in
 	  let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
 	    Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
       | IsCoFixpoint ->
@@ -254,10 +262,10 @@ let red = Reductionops.nf_betaiota
 let init_prog_info n b t deps fixkind notations obls impls kind hook =
   let obls' = 
     Array.mapi
-      (fun i (n, t, o, d) ->
+      (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_type = red t; obl_opaque = o;
+	   obl_location = l; obl_type = red t; obl_opaque = o;
 	   obl_deps = d })
       obls
   in
@@ -346,6 +354,7 @@ let obligations_of_evars evars =
 	 (fun (n, t) ->
 	    { obl_name = n;
 	      obl_type = t;
+	      obl_location = dummy_loc;
 	      obl_body = None;
 	      obl_opaque = false;
 	      obl_deps = Intset.empty;
@@ -397,7 +406,7 @@ and solve_obligation_by_tac prg obls i tac =
       Some _ -> false
     | None -> 
 	(try
-	   if deps_remaining obls obl.obl_deps = [] then
+	    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 
@@ -405,8 +414,12 @@ and solve_obligation_by_tac prg obls i tac =
 	       else
 		 obls.(i) <- { obl with obl_body = Some t };
 	       true		 
-	   else false
-	 with _ -> false)  
+	    else false
+	  with
+	    | Stdpp.Exc_located(_, Refiner.FailError (_, s))
+	    | Refiner.FailError (_, s) ->
+		user_err_loc (obl.obl_location, "solve_obligation", s)
+	    | e -> false)
 
 and solve_prg_obligations prg tac = 
   let obls, rem = prg.prg_obligations in
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 8ed6ce7e44..997c2479de 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -1,8 +1,8 @@
 open Names
 open Util
 
-type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array
-    (* ident, type, opaque or transparent, dependencies *)
+type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array
+    (* ident, type, location, opaque or transparent, dependencies *)
 
 type progress = (* Resolution status of a program *)
     | Remain of int  (* n obligations remaining *)
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 647db2c9c5..4af18f52d3 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -373,7 +373,7 @@ let solve_by_tac evi t =
       Pfedit.delete_current_proof (); const.Entries.const_entry_body
   with e ->
     Pfedit.delete_current_proof();
-    raise Exit
+    raise e
 
 (* let apply_tac t goal = t goal *)