Refl_tauto (coq-core.Rtauto_plugin.Refl

type atom_env = {

mutable next : int;

mutable env : (Constr.t * int) list;

}

val make_form : Environ.env -> Evd.evar_map -> atom_env -> EConstr.types -> Proof_search.form

val make_hyps : Environ.env -> Evd.evar_map -> atom_env -> EConstr.types list -> EConstr.named_context -> (Names.Id.t Context.binder_annot * Proof_search.form) list

val rtauto_tac : unit Proofview.tactic