let id_tac =
let id_tac (proof,goal) =
- let _, metasenv, _, _ = proof in
+ let _, metasenv, _, _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
(proof,[goal])
in
let fail_tac =
let fail_tac (proof,goal) =
- let _, metasenv, _, _ = proof in
+ let _, metasenv, _, _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
raise (PET.Fail (lazy "fail tactical"))
in
let progress_tactic ~tactic =
let msg = lazy "Failed to progress" in
let get_sequent (proof, goal) =
- let (_, metasenv, _, _) = proof in
+ let (_, metasenv, _, _, _) = proof in
let _, context, ty = CicUtil.lookup_meta goal metasenv in
context, ty
in