Module Aac_rewrite

module Aac_rewrite: sig .. end

aac_rewrite -- rewriting modulo A or AC


val aac_reflexivity : Coq.goal_sigma -> Proof_type.goal list Evd.sigma
val aac_normalise : Coq.goal_sigma -> Proof_type.goal list Evd.sigma
val aac_rewrite : args:(string * int) list ->
?abort:bool ->
EConstr.constr ->
?l2r:bool ->
?show:bool -> ?strict:bool -> ?extra:EConstr.t -> Proof_type.tactic
val add : string -> 'a -> (string * 'a) list -> (string * 'a) list
val pr_aac_args : 'a -> 'b -> 'c -> (string * int) list -> Pp.t