sig
  type envs
  val empty_envs : unit -> AAC_theory.Trans.envs
  val t_of_constr :
    AAC_coq.goal_sigma ->
    AAC_coq.Relation.t ->
    AAC_theory.Trans.envs ->
    Term.constr * Term.constr ->
    AAC_matcher.Terms.t * AAC_matcher.Terms.t * AAC_coq.goal_sigma
  val add_symbol :
    AAC_coq.goal_sigma ->
    AAC_coq.Relation.t ->
    AAC_theory.Trans.envs -> Term.constr -> AAC_coq.goal_sigma
  type ir
  val ir_of_envs :
    AAC_coq.goal_sigma ->
    AAC_coq.Relation.t ->
    AAC_theory.Trans.envs -> AAC_coq.goal_sigma * AAC_theory.Trans.ir
  val ir_to_units : AAC_theory.Trans.ir -> AAC_matcher.ext_units
  val raw_constr_of_t :
    AAC_theory.Trans.ir ->
    AAC_coq.Relation.t ->
    Term.rel_context -> AAC_matcher.Terms.t -> Term.constr
  type sigmas = {
    env_sym : Term.constr;
    env_bin : Term.constr;
    env_units : Term.constr;
  }
  type reifier
  val mk_reifier :
    AAC_coq.Relation.t ->
    Term.constr ->
    AAC_theory.Trans.ir ->
    (AAC_theory.Trans.sigmas * AAC_theory.Trans.reifier -> Proof_type.tactic) ->
    Proof_type.tactic
  val reif_constr_of_t :
    AAC_theory.Trans.reifier -> AAC_matcher.Terms.t -> Term.constr
end