Module `Rtauto_plugin.Refl_tauto`

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