sig
  type tactic = unit Proofview.tactic
  type lazy_ref = Names.GlobRef.t Stdlib.Lazy.t
  val get_fresh : Coq.lazy_ref -> Constr.constr
  val get_efresh : Coq.lazy_ref -> EConstr.constr
  val find_global : string -> Coq.lazy_ref
  val cps_resolve_one_typeclass :
    ?error:Pp.t ->
    EConstr.types -> (EConstr.constr -> Coq.tactic) -> Coq.tactic
  val evar_binary :
    Environ.env ->
    Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
  val evar_relation :
    Environ.env ->
    Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
  val mk_letin : string -> EConstr.constr -> EConstr.constr Proofview.tactic
  val tclRETYPE : EConstr.constr -> unit Proofview.tactic
  val decomp_term :
    Evd.evar_map ->
    EConstr.constr ->
    (EConstr.constr, EConstr.types, EConstr.ESorts.t, EConstr.EInstance.t,
     EConstr.ERelevance.t)
    Constr.kind_of_term
  module List :
    sig
      val of_list : EConstr.constr -> EConstr.constr list -> EConstr.constr
      val type_of_list : EConstr.constr -> EConstr.constr
    end
  module Pair :
    sig
      val typ : Coq.lazy_ref
      val pair : Coq.lazy_ref
      val of_pair :
        EConstr.constr ->
        EConstr.constr -> EConstr.constr * EConstr.constr -> EConstr.constr
    end
  module Option :
    sig
      val typ : Coq.lazy_ref
      val some : EConstr.constr -> EConstr.constr -> EConstr.constr
      val none : EConstr.constr -> EConstr.constr
      val of_option :
        EConstr.constr -> EConstr.constr option -> EConstr.constr
    end
  module Pos :
    sig val typ : Coq.lazy_ref val of_int : int -> EConstr.constr end
  module Nat :
    sig val typ : Coq.lazy_ref val of_int : int -> Constr.constr end
  module Classes :
    sig
      val mk_morphism :
        EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
      val mk_equivalence : EConstr.constr -> EConstr.constr -> EConstr.constr
      val mk_reflexive : EConstr.constr -> EConstr.constr -> EConstr.constr
      val mk_transitive : EConstr.constr -> EConstr.constr -> EConstr.constr
    end
  module Relation :
    sig
      type t = { carrier : EConstr.constr; r : EConstr.constr; }
      val make : EConstr.constr -> EConstr.constr -> Coq.Relation.t
      val split : Coq.Relation.t -> EConstr.constr * EConstr.constr
    end
  module Equivalence :
    sig
      type t = {
        carrier : EConstr.constr;
        eq : EConstr.constr;
        equivalence : EConstr.constr;
      }
      val make :
        EConstr.constr ->
        EConstr.constr -> EConstr.constr -> Coq.Equivalence.t
      val infer :
        Environ.env ->
        Evd.evar_map ->
        EConstr.constr -> EConstr.constr -> Coq.Equivalence.t * Evd.evar_map
      val from_relation :
        Environ.env ->
        Evd.evar_map -> Coq.Relation.t -> Coq.Equivalence.t * Evd.evar_map
      val to_relation : Coq.Equivalence.t -> Coq.Relation.t
      val split :
        Coq.Equivalence.t -> EConstr.constr * EConstr.constr * EConstr.constr
    end
  val match_as_equation :
    ?context:EConstr.rel_context ->
    Environ.env ->
    Evd.evar_map ->
    EConstr.constr ->
    (EConstr.constr * EConstr.constr * Coq.Relation.t) option
  val tclTIME : string -> Coq.tactic -> Coq.tactic
  val tclDEBUG : string -> unit Proofview.tactic
  val tclPRINT : unit Proofview.tactic
  val anomaly : string -> 'a
  val user_error : Pp.t -> 'a
  val warning : string -> unit
  val show_proof : Declare.Proof.t -> unit
  module Rewrite :
    sig
      type hypinfo = {
        hyp : EConstr.constr;
        hyptype : EConstr.constr;
        context : EConstr.rel_context;
        body : EConstr.constr;
        rel : Coq.Relation.t;
        left : EConstr.constr;
        right : EConstr.constr;
        l2r : bool;
      }
      val get_hypinfo :
        Environ.env ->
        Evd.evar_map ->
        ?check_type:(EConstr.types -> bool) ->
        EConstr.constr -> l2r:bool -> Coq.Rewrite.hypinfo
      val build :
        Coq.Rewrite.hypinfo -> (int * EConstr.constr) list -> EConstr.constr
      val rewrite :
        ?abort:bool ->
        Coq.Rewrite.hypinfo ->
        (int * EConstr.constr) list -> unit Proofview.tactic
    end
end