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