+ let progress_tactic ~tactic =
+ let msg = lazy "Failed to progress" in
+ let get_sequent (proof, goal) =
+ let (_, metasenv, _, _) = proof in
+ let _, context, ty = CicUtil.lookup_meta goal metasenv in
+ context, ty
+ in
+ let progress_tactic ist =
+ let before = get_sequent (S.get_status ist) in
+ let ost = S.apply_tactic tactic ist in
+ match S.goals ost with
+ | [goal], _ when before <> get_sequent (S.get_proof ost, goal) ->
+ raise (PET.Fail msg)
+ | _ -> ost
+ in
+ S.mk_tactic progress_tactic
+