Imported Upstream version 8.3pl1upstream/8.3pl1

4 files changed, 16 insertions, 16 deletions

diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index f1bdd640..3fb6824b 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -28,7 +28,7 @@ type oblinfo =
     ev_hyps: named_context;
     ev_status: obligation_definition_status;
     ev_chop: int option;
-    ev_loc: Util.loc;
+    ev_source: hole_kind located;
     ev_typ: types;
     ev_tac: tactic option;
     ev_deps: Intset.t }
@@ -218,9 +218,9 @@ let eterm_obligations env name isevars evm fs ?status t ty =
 	       else None
 	   | None -> 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; ev_tac = tac }
+	 let info = { ev_name = (n, nstr); ev_hyps = hyps; 
+		      ev_status = status; ev_chop = chop;
+		      ev_source = (loc, k); ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
 	 in (id, info) :: l)
       evn []
   in
@@ -231,12 +231,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_source = source; 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, source, 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 262889c8..2abc25a3 100644
--- a/plugins/subtac/eterm.mli
+++ b/plugins/subtac/eterm.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: eterm.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: eterm.mli 13693 2010-12-08 15:32:25Z msozeau $ i*)
 open Environ
 open Tacmach
 open Term
@@ -24,7 +24,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 b76d0cb0..d3a63410 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_source : hole_kind located;
     obl_body : constr option;
     obl_status : obligation_definition_status;
     obl_deps : Intset.t;
@@ -307,14 +307,14 @@ 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_source = (dummy_loc, QuestionMark Expand); obl_type = t;
 	       obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } |],
 	mkVar n
     | Some b ->
 	Array.mapi
 	  (fun i (n, t, l, o, d, tac) ->
             { obl_name = n ; obl_body = None; 
-	      obl_location = l; obl_type = reduce t; obl_status = o;
+	      obl_source = l; obl_type = reduce t; obl_status = o;
 	      obl_deps = d; obl_tac = tac })
 	  obls, b
   in
@@ -488,7 +488,7 @@ and solve_obligation_by_tac prg obls i tac =
 	| Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
 	| Stdpp.Exc_located(_, Refiner.FailError (_, s))
 	| Refiner.FailError (_, s) ->
-	    user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s)
+	    user_err_loc (fst obl.obl_source, "solve_obligation", Lazy.force s)
 	| e -> false
 
 and solve_prg_obligations prg tac =
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index bc5fc3e1..5f6d1a2e 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -6,9 +6,9 @@ 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),
+    (* ident, type, source, (opaque or transparent, expand or define),
        dependencies, tactic to solve it *)
 
 type progress = (* Resolution status of a program *)