diff options
Diffstat (limited to 'plugins/subtac/eterm.ml')
| -rw-r--r-- | plugins/subtac/eterm.ml | 12 |
1 files changed, 6 insertions, 6 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 |