in
aux (n-1) tl
(status_of_single_goal_tactic_result
- (ProofEngineTypes.apply_tactic (S.clear ~hyp:name_of_hyp) status))
+ (ProofEngineTypes.apply_tactic (S.clear ~hyps:[name_of_hyp]) status))
| (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
in
let (_, metasenv, _, _) = proof in