Keep obligation source information in Program

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

4 files changed, 11 insertions, 11 deletions

diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index 9790667c42..5ed335d040 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -27,7 +27,7 @@ type oblinfo =
     ev_hyps: named_context;
     ev_status: obligation_definition_status;
     ev_chop: int option;
-    ev_loc: Util.loc;
+    ev_src: hole_kind located;
     ev_typ: types;
     ev_tac: tactic option;
     ev_deps: Intset.t }
@@ -223,7 +223,7 @@ let eterm_obligations env name isevars evm fs ?status t ty =
 	 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; ev_tac = tac }
+		      ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
 	 in (id, info) :: l)
       evn []
   in
@@ -234,12 +234,12 @@ let eterm_obligations env name isevars evm fs ?status t ty =
   let evars = 
     List.map (fun (ev, info) ->
       let { ev_name = (_, name); ev_status = status;
-	    ev_loc = loc; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
+	    ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
       in
       let status = match status with
 	| Define true when Idset.mem name transparent -> Define false
 	| _ -> status
-      in name, typ, loc, status, deps, tac) evts
+      in name, typ, src, 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
diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli
index f827b9237c..03d76f29a6 100644
--- a/plugins/subtac/eterm.mli
+++ b/plugins/subtac/eterm.mli
@@ -23,7 +23,7 @@ val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info *
    evars contexts, object and type *)
 val eterm_obligations : env -> identifier -> evar_map -> evar_map -> int ->
   ?status:obligation_definition_status -> constr -> types -> 
-  (identifier * types * loc * obligation_definition_status * Intset.t * 
+  (identifier * types * hole_kind located * obligation_definition_status * Intset.t * 
       tactic option) array
     (* Existential key, obl. name, type as product, location of the original evar, associated tactic,
        status and dependencies as indexes into the array *)
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 18752c9f9a..aa018d4f28 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -30,13 +30,13 @@ 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 * obligation_definition_status * Intset.t
-			 * tactic option) array
+type obligation_info = (Names.identifier * Term.types * hole_kind located *
+			  obligation_definition_status * Intset.t * tactic option) array
 
 type obligation =
   { obl_name : identifier;
     obl_type : types;
-    obl_location : loc;
+    obl_location : hole_kind located;
     obl_body : constr option;
     obl_status : obligation_definition_status;
     obl_deps : Intset.t;
@@ -364,7 +364,7 @@ let init_prog_info n b t deps fixkind notations obls impls kind reduce hook =
 	assert(obls = [||]);
 	let n = Nameops.add_suffix n "_obligation" in
 	  [| { obl_name = n; obl_body = None;
-	       obl_location = dummy_loc; obl_type = t;
+	       obl_location = dummy_loc, InternalHole; obl_type = t;
 	       obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } |],
 	mkVar n
     | Some b ->
@@ -545,7 +545,7 @@ and solve_obligation_by_tac prg obls i tac =
 	| Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
 	| Loc.Exc_located(_, Refiner.FailError (_, s))
 	| Refiner.FailError (_, s) ->
-	    user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s)
+	    user_err_loc (unloc obl.obl_location, "solve_obligation", Lazy.force s)
 	| Util.Anomaly _ as e -> raise e
 	| e -> false
 
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index bc5fc3e100..c1d665aaca 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -6,7 +6,7 @@ open Proof_type
 open Vernacexpr
 
 type obligation_info =
-  (identifier * Term.types * loc *
+  (identifier * Term.types * hole_kind located *
       obligation_definition_status * Intset.t * tactic option) array
     (* ident, type, location, (opaque or transparent, expand or define),
        dependencies, tactic to solve it *)