sig
  module type ARG =
    sig
      type t
      val equal : Traversal.ARG.t -> Traversal.ARG.t -> bool
      val hash : Traversal.ARG.t -> int
      val print : Traversal.ARG.t CCFormat.printer
      val section : Utils.Section.t
      val fail : ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
    end
  module Make :
    functor (T : TermInner.S) (Arg : ARG) (State : sig type t end) ->
      sig
        type term = T.t
        type ty = T.t
        type t
        type dispatch = {
          do_term :
            Traversal.Make.t ->
            depth:int -> Traversal.Make.term -> Traversal.Make.term;
          do_goal_or_axiom :
            (Traversal.Make.t ->
             depth:int ->
             [ `Axiom | `Goal ] -> Traversal.Make.term -> Traversal.Make.term)
            option;
          do_def :
            Traversal.Make.t ->
            depth:int ->
            (Traversal.Make.term, Traversal.Make.ty) Statement.rec_def ->
            Arg.t ->
            (Traversal.Make.term, Traversal.Make.ty) Statement.rec_def;
          do_pred :
            Traversal.Make.t ->
            depth:int ->
            [ `Not_wf | `Wf ] ->
            [ `Copred | `Pred ] ->
            (Traversal.Make.term, Traversal.Make.ty) Statement.pred_def ->
            Arg.t ->
            (Traversal.Make.term, Traversal.Make.ty) Statement.pred_def;
          do_copy :
            (Traversal.Make.t ->
             depth:int ->
             loc:Location.t option ->
             (Traversal.Make.term, Traversal.Make.ty) Statement.copy ->
             Arg.t -> (Traversal.Make.term, Traversal.Make.ty) Statement.copy)
            option;
          do_spec :
            (Traversal.Make.t ->
             depth:int ->
             loc:Location.t option ->
             ID.t ->
             (Traversal.Make.term, Traversal.Make.ty) Statement.spec_defs ->
             Arg.t ->
             (Traversal.Make.term, Traversal.Make.ty) Statement.spec_defs)
            option;
          do_data :
            (Traversal.Make.t ->
             depth:int ->
             [ `Codata | `Data ] ->
             Traversal.Make.term Statement.tydef ->
             Arg.t -> Traversal.Make.term Statement.tydef)
            option;
          do_ty_def :
            (Traversal.Make.t ->
             ?loc:Location.t ->
             attrs:Statement.decl_attr list ->
             ID.t ->
             ty:Traversal.Make.ty ->
             Arg.t -> ID.t * Traversal.Make.ty * Statement.decl_attr list)
            option;
        }
        val create :
          ?size:int ->
          ?max_depth:int ->
          env:(Traversal.Make.term, Traversal.Make.ty) Env.t ->
          state:State.t ->
          dispatch:Traversal.Make.dispatch -> unit -> Traversal.Make.t
        val env :
          Traversal.Make.t -> (Traversal.Make.term, Traversal.Make.ty) Env.t
        val state : Traversal.Make.t -> State.t
        val has_processed : Traversal.Make.t -> ID.t -> Arg.t -> bool
        val mark_processed : Traversal.Make.t -> ID.t -> Arg.t -> unit
        val processed : Traversal.Make.t -> (ID.t * Arg.t) Sequence.t
        val call_dep : Traversal.Make.t -> depth:int -> ID.t -> Arg.t -> unit
        exception CannotTraverse
        val traverse_stmt :
          ?after_env:((Traversal.Make.term, Traversal.Make.ty) Env.t -> unit) ->
          Traversal.Make.t ->
          (Traversal.Make.term, Traversal.Make.ty) Statement.t -> unit
        val get_statements :
          Traversal.Make.t ->
          (Traversal.Make.term, Traversal.Make.ty) Statement.t
          CCVector.vector
        val max_depth_reached : Traversal.Make.t -> bool
      end
end