sig
  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 -> '-> (string * 'a) list -> (string * 'a) list
  val pr_aac_args : '-> '-> '-> (string * int) list -> Pp.t
end