in
mk_tactic (clearbody ~hyp)
-let clear ~hyp =
- let clear ~hyp (proof, goal) =
+let clear_one ~hyp =
+ let clear_one ~hyp (proof, goal) =
let module C = Cic in
let curi,metasenv,pbo,pty = proof in
let metano,context,ty =
in
(curi,metasenv',pbo,pty), [goal]
in
- mk_tactic (clear ~hyp)
+ 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)
(* Warning: this tactic has no effect on the proof term.
It just changes the name of an hypothesis in the current sequent *)