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
in
PET.mk_tactic if_
+let ifs ~start ~continuations ~fail =
+ let ifs status =
+ let xoutput =
+ try
+ let result = PET.apply_tactic start status in
+ info (lazy ("Tacticals.ifs: succedeed!!!"));
+ Some result
+ with PET.Fail _ -> None
+ in
+ let tactic = match xoutput with
+ | Some res -> thens ~start:(const_tac res) ~continuations
+ | None -> fail
+ in
+ PET.apply_tactic tactic status
+ in
+ PET.mk_tactic ifs
+
let first ~tactics =
let rec first ~(tactics: tactic list) status =
info (lazy "in Tacticals.first");
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