sig
  type envs
  val empty_envs : unit -> Theory.Trans.envs
  val t_of_constr :
    Environ.env ->
    Evd.evar_map ->
    Coq.Relation.t ->
    Theory.Trans.envs ->
    EConstr.constr * EConstr.constr ->
    Matcher.Terms.t * Matcher.Terms.t * Evd.evar_map
  val add_symbol :
    Environ.env ->
    Evd.evar_map ->
    Coq.Relation.t -> Theory.Trans.envs -> Constr.t -> Evd.evar_map
  type ir
  val ir_of_envs :
    Environ.env ->
    Evd.evar_map ->
    Coq.Relation.t -> Theory.Trans.envs -> Evd.evar_map * Theory.Trans.ir
  val ir_to_units : Theory.Trans.ir -> Matcher.ext_units
  val raw_constr_of_t :
    Theory.Trans.ir ->
    Coq.Relation.t ->
    EConstr.rel_context -> Matcher.Terms.t -> EConstr.constr
  type sigmas = {
    env_sym : EConstr.constr;
    env_bin : EConstr.constr;
    env_units : EConstr.constr;
  }
  type reifier
  val mk_reifier :
    Coq.Relation.t ->
    EConstr.constr ->
    Theory.Trans.ir ->
    (Theory.Trans.sigmas * Theory.Trans.reifier) Proofview.tactic
  val reif_constr_of_t :
    Theory.Trans.reifier -> Matcher.Terms.t -> EConstr.constr
end