let id_tac =
let id_tac (proof,goal) =
- let _, metasenv, _subst, _, _, _ = 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, _subst, _ , _, _ = 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 progress_tactic (((_,metasenv,_subst,_,_,_),g) as istatus) =
- let ((_,metasenv',_subst,_,_,_),opened) as ostatus =
+ let progress_tactic (((_,metasenv,_,_,_,_),g) as istatus) =
+ let ((_,metasenv',_,_,_,_),opened) as ostatus =
PET.apply_tactic tactic istatus
in
match opened with
| [g1] ->
- let _,_,oldty = CicUtil.lookup_meta g metasenv in
- let _,_,newty = CicUtil.lookup_meta g1 metasenv' in
- if oldty = newty then
+ let _,oc,oldty = CicUtil.lookup_meta g metasenv in
+ let _,nc,newty = CicUtil.lookup_meta g1 metasenv' in
+ if oldty = newty && oc = nc then
raise (PET.Fail msg)
else
ostatus