let absurd_tac ~term =
let absurd_tac ~term status =
let (proof, goal) = status in
let absurd_tac ~term =
let absurd_tac ~term status =
let (proof, goal) = status in
(* sarebbe piu' elegante se Assumtion sollevasse un'eccezione tutta sua che questa cattura, magari con l'aiuto di try_tactics *)
in
ProofEngineTypes.mk_tactic contradiction_tac
(* sarebbe piu' elegante se Assumtion sollevasse un'eccezione tutta sua che questa cattura, magari con l'aiuto di try_tactics *)
in
ProofEngineTypes.mk_tactic contradiction_tac