sig
  val mk_mset :
    EConstr.constr -> (EConstr.constr * int) list -> EConstr.constr
  module Sigma :
    sig
      val add :
        EConstr.constr ->
        EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
      val empty : EConstr.constr -> EConstr.constr
      val of_list :
        EConstr.constr ->
        EConstr.constr -> (int * EConstr.constr) list -> EConstr.constr
      val to_fun :
        EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
    end
  module Sym :
    sig
      type pack = { ar : Constr.t; value : Constr.t; morph : Constr.t; }
      val typ : Coq.lazy_ref
      val mk_pack : Coq.Relation.t -> Theory.Sym.pack -> EConstr.constr
      val null : Coq.Relation.t -> EConstr.constr
    end
  module Stubs :
    sig
      val lift : Coq.lazy_ref
      val lift_proj_equivalence : Coq.lazy_ref
      val lift_transitivity_left : Coq.lazy_ref
      val lift_transitivity_right : Coq.lazy_ref
      val lift_reflexivity : Coq.lazy_ref
      val eval : Coq.lazy_ref
      val decide_thm : Coq.lazy_ref
      val lift_normalise_thm : Coq.lazy_ref
    end
  module Trans :
    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
end