diff options
Diffstat (limited to 'plugins/subtac/eterm.ml')
| -rw-r--r-- | plugins/subtac/eterm.ml | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml index 3fb6824b..5ed335d0 100644 --- a/plugins/subtac/eterm.ml +++ b/plugins/subtac/eterm.ml @@ -1,4 +1,3 @@ -(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *) (** - Get types of existentials ; - Flatten dependency tree (prefix order) ; @@ -28,11 +27,15 @@ type oblinfo = ev_hyps: named_context; ev_status: obligation_definition_status; ev_chop: int option; - ev_source: hole_kind located; + ev_src: hole_kind located; ev_typ: types; ev_tac: tactic option; ev_deps: Intset.t } +(* spiwack: Store field for internalizing ev_tac in evar_infos' evar_extra. *) +open Store.Field +let evar_tactic = Store.field () + (** Substitute evar references in t using De Bruijn indices, where n binders were passed through. *) @@ -210,7 +213,7 @@ let eterm_obligations env name isevars evm fs ?status t ty = | Some s -> s, None | None -> Define true, None in - let tac = match ev.evar_extra with + let tac = match evar_tactic.get ev.evar_extra with | Some t -> if Dyn.tag t = "tactic" then Some (Tacinterp.interp @@ -218,9 +221,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_source = (loc, k); 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_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac } in (id, info) :: l) evn [] in @@ -231,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_source = source; 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, source, 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 |