let id_tac =
let id_tac (proof,goal) =
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = 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, _subst, _ , _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
raise (PET.Fail (lazy "fail tactical"))
in
back to obtain the result of the tactic *)
let mk_tactic f =
PET.mk_tactic
- (fun (proof, goal) as pstatus ->
+ (fun ((proof, goal) as pstatus) ->
let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
let istatus = pstatus, stack in
let (proof, _, _), stack = f istatus in
let progress_tactic ~tactic =
let msg = lazy "Failed to progress" in
- let progress_tactic (((_,metasenv,_,_,_),_) as istatus) =
- let ((_,metasenv',_,_,_),_) as ostatus =
+ let progress_tactic (((_,metasenv,_subst,_,_,_),_) as istatus) =
+ let ((_,metasenv',_subst,_,_,_),_) as ostatus =
PET.apply_tactic tactic istatus
in
(*CSC: Warning