sig
  val init_constant : string list -> string -> Term.constr
  type goal_sigma = Proof_type.goal Tacmach.sigma
  val goal_update : Coq.goal_sigma -> Evd.evar_map -> Coq.goal_sigma
  val resolve_one_typeclass :
    Proof_type.goal Tacmach.sigma ->
    Term.types -> Term.constr * Coq.goal_sigma
  val cps_resolve_one_typeclass :
    ?error:string ->
    Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic
  val nf_evar : Coq.goal_sigma -> Term.constr -> Term.constr
  val fresh_evar :
    Coq.goal_sigma -> Term.types -> Term.constr * Coq.goal_sigma
  val evar_unit :
    Coq.goal_sigma -> Term.constr -> Term.constr * Coq.goal_sigma
  val evar_binary :
    Coq.goal_sigma -> Term.constr -> Term.constr * Coq.goal_sigma
  val evar_relation :
    Coq.goal_sigma -> Term.constr -> Term.constr * Coq.goal_sigma
  val cps_evar_relation :
    Term.constr -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic
  val cps_mk_letin :
    string ->
    Term.constr -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic
  val decomp_term :
    Term.constr -> (Term.constr, Term.types) Term.kind_of_term
  val lapp : Term.constr lazy_t -> Term.constr array -> Term.constr
  module List :
    sig
      val of_list : Term.constr -> Term.constr list -> Term.constr
      val type_of_list : Term.constr -> Term.constr
    end
  module Pair :
    sig
      val typ : Term.constr lazy_t
      val pair : Term.constr lazy_t
      val of_pair :
        Term.constr ->
        Term.constr -> Term.constr * Term.constr -> Term.constr
    end
  module Bool :
    sig val typ : Term.constr lazy_t val of_bool : bool -> Term.constr end
  module Comparison :
    sig
      val typ : Term.constr lazy_t
      val eq : Term.constr lazy_t
      val lt : Term.constr lazy_t
      val gt : Term.constr lazy_t
    end
  module Leibniz :
    sig
      val eq_refl : Term.types -> Term.constr -> Term.constr
      val eq : Term.types -> Term.constr
    end
  module Option :
    sig
      val some : Term.constr -> Term.constr -> Term.constr
      val none : Term.constr -> Term.constr
      val of_option : Term.constr -> Term.constr option -> Term.constr
    end
  module Pos :
    sig val typ : Term.constr lazy_t val of_int : int -> Term.constr end
  module Nat :
    sig val typ : Term.constr lazy_t val of_int : int -> Term.constr end
  module Classes :
    sig
      val mk_morphism :
        Term.constr -> Term.constr -> Term.constr -> Term.constr
      val mk_equivalence : Term.constr -> Term.constr -> Term.constr
      val mk_reflexive : Term.constr -> Term.constr -> Term.constr
      val mk_transitive : Term.constr -> Term.constr -> Term.constr
    end
  module Relation :
    sig
      type t = { carrier : Term.constr; r : Term.constr; }
      val make : Term.constr -> Term.constr -> Coq.Relation.t
      val split : Coq.Relation.t -> Term.constr * Term.constr
    end
  module Transitive :
    sig
      type t = {
        carrier : Term.constr;
        leq : Term.constr;
        transitive : Term.constr;
      }
      val make :
        Term.constr -> Term.constr -> Term.constr -> Coq.Transitive.t
      val infer :
        Coq.goal_sigma ->
        Term.constr -> Term.constr -> Coq.Transitive.t * Coq.goal_sigma
      val from_relation :
        Coq.goal_sigma -> Coq.Relation.t -> Coq.Transitive.t * Coq.goal_sigma
      val cps_from_relation :
        Coq.Relation.t ->
        (Coq.Transitive.t -> Proof_type.tactic) -> Proof_type.tactic
      val to_relation : Coq.Transitive.t -> Coq.Relation.t
    end
  module Equivalence :
    sig
      type t = {
        carrier : Term.constr;
        eq : Term.constr;
        equivalence : Term.constr;
      }
      val make :
        Term.constr -> Term.constr -> Term.constr -> Coq.Equivalence.t
      val infer :
        Coq.goal_sigma ->
        Term.constr -> Term.constr -> Coq.Equivalence.t * Coq.goal_sigma
      val from_relation :
        Coq.goal_sigma ->
        Coq.Relation.t -> Coq.Equivalence.t * Coq.goal_sigma
      val cps_from_relation :
        Coq.Relation.t ->
        (Coq.Equivalence.t -> Proof_type.tactic) -> Proof_type.tactic
      val to_relation : Coq.Equivalence.t -> Coq.Relation.t
      val split :
        Coq.Equivalence.t -> Term.constr * Term.constr * Term.constr
    end
  val match_as_equation :
    ?context:Term.rel_context ->
    Coq.goal_sigma ->
    Term.constr -> (Term.constr * Term.constr * Coq.Relation.t) option
  val tclTIME : string -> Proof_type.tactic -> Proof_type.tactic
  val tclDEBUG : string -> Proof_type.tactic -> Proof_type.tactic
  val tclPRINT : Proof_type.tactic -> Proof_type.tactic
  val anomaly : string -> 'a
  val user_error : string -> 'a
  val warning : string -> unit
  module Rewrite :
    sig
      type hypinfo = {
        hyp : Term.constr;
        hyptype : Term.constr;
        context : Term.rel_context;
        body : Term.constr;
        rel : Coq.Relation.t;
        left : Term.constr;
        right : Term.constr;
        l2r : bool;
      }
      val get_hypinfo :
        Term.constr ->
        l2r:bool ->
        ?check_type:(Term.types -> bool) ->
        (Coq.Rewrite.hypinfo -> Proof_type.tactic) -> Proof_type.tactic
      val build :
        Coq.Rewrite.hypinfo ->
        (int * Term.constr) list ->
        (Term.constr -> Proof_type.tactic) -> Proof_type.tactic
      val build_with_evar :
        Coq.Rewrite.hypinfo ->
        (int * Term.constr) list ->
        (Term.constr -> Proof_type.tactic) -> Proof_type.tactic
      val rewrite :
        ?abort:bool ->
        Coq.Rewrite.hypinfo ->
        (int * Term.constr) list ->
        (Proof_type.tactic -> Proof_type.tactic) -> Proof_type.tactic
    end
end