if b then n else find (n+1) tl
| _ -> find (n+1) tl
)
- | [] -> raise (PET.Fail "Assumption: No such assumption")
+ | [] -> raise (PET.Fail (lazy "Assumption: No such assumption"))
in PET.apply_tactic (PT.apply_tac ~term:(C.Rel (find 1 context))) status
in
PET.mk_tactic assumption_tac