(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* unit Proofview.tactic val contradiction : constr with_bindings option -> unit Proofview.tactic