Module `Cc_plugin.Cctac`

val proof_tac : Ccproof.proof -> unit Proofview.tactic
val cc_tactic : int -> EConstr.constr list -> bool -> unit Proofview.tactic
val congruence_tac : int -> EConstr.constr list -> unit Proofview.tactic
val simple_congruence_tac : int -> EConstr.constr list -> unit Proofview.tactic
val f_equal : unit Proofview.tactic