diff options
Diffstat (limited to 'plugins/subtac')
| -rw-r--r-- | plugins/subtac/eterm.ml | 12 | ||||
| -rw-r--r-- | plugins/subtac/eterm.mli | 4 | ||||
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 12 | ||||
| -rw-r--r-- | plugins/subtac/subtac_obligations.mli | 4 |
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 *) |