summaryrefslogtreecommitdiff
path: root/plugins/subtac
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-12-24 11:53:29 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2010-12-24 11:53:29 +0100
commit6b691bbd2101fd39395c0d2135fd7c06a8915e14 (patch)
treeb04b45d1a6f42d19b1428c522d647afbad2f9b83 /plugins/subtac
parent3e96002677226c0cdaa8f355938a76cfb37a722a (diff)
Imported Upstream version 8.3pl1upstream/8.3pl1
Diffstat (limited to 'plugins/subtac')
-rw-r--r--plugins/subtac/eterm.ml12
-rw-r--r--plugins/subtac/eterm.mli4
-rw-r--r--plugins/subtac/subtac_obligations.ml12
-rw-r--r--plugins/subtac/subtac_obligations.mli4
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 *)