+ mk_tactic (clear_one ~hyp)
+
+let clear ~hyps =
+ let clear hyps status =
+ let aux status hyp =
+ match apply_tactic (clear_one ~hyp) status with
+ | proof, [g] -> proof, g
+ | _ -> raise (Fail (lazy "clear: internal error"))
+ in
+ let proof, g = List.fold_left aux status hyps in
+ proof, [g]
+ in
+ mk_tactic (clear hyps)