diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-12-24 11:53:29 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-12-24 11:53:29 +0100 |
| commit | 6b691bbd2101fd39395c0d2135fd7c06a8915e14 (patch) | |
| tree | b04b45d1a6f42d19b1428c522d647afbad2f9b83 /plugins/subtac/eterm.ml | |
| parent | 3e96002677226c0cdaa8f355938a76cfb37a722a (diff) | |
Imported Upstream version 8.3pl1upstream/8.3pl1
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 |