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,_,_,_),_) as istatus) =
- let ((_,metasenv',_subst,_,_,_),_) as ostatus =
+ let progress_tactic (((_,metasenv,_,_,_,_),g) as istatus) =
+ let ((_,metasenv',_,_,_,_),opened) as ostatus =
PET.apply_tactic tactic istatus
in
- (*CSC: Warning
- If just the index of some metas changes the tactic is recognized
- as a progressing one. This is wrong. *)
- if metasenv' = metasenv then
- raise (PET.Fail msg)
- else
- ostatus
+ match opened with
+ | [g1] ->
+ 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
+ | _ -> ostatus
in
PET.mk_tactic progress_tactic