type __ = Obj.t type nat = | O | S of nat type ('a, 'b) prod = | Pair of 'a * 'b type 'a sig0 = 'a (* singleton inductive, whose constructor was exist *) val plus : nat -> nat -> nat type 'a list = | Nil | Cons of 'a * 'a list val app : 'a1 list -> 'a1 list -> 'a1 list type 'x compare = | Lt | Eq | Gt module type OrderedType = sig type t val compare : t -> t -> t compare end module MoreOrderedType : functor (O:OrderedType) -> sig val eq_dec : O.t -> O.t -> bool val lt_dec : O.t -> O.t -> bool end type positive = | XI of positive | XO of positive | XH type z = | ZERO | POS of positive | NEG of positive type relation = | EGAL | INFERIEUR | SUPERIEUR val add_un : positive -> positive val add : positive -> positive -> positive val add_carry : positive -> positive -> positive val double_moins_un : positive -> positive val compare0 : positive -> positive -> relation -> relation type entier = | Nul | Pos of positive val un_suivi_de : entier -> entier val zero_suivi_de : entier -> entier val double_moins_deux : positive -> entier val sub_pos : positive -> positive -> entier val sub_neg : positive -> positive -> entier val op : relation -> relation val zplus : z -> z -> z val times : positive -> positive -> positive val zmult : z -> z -> z val zcompare : z -> z -> relation val lt_eq_lt_dec : nat -> nat -> bool option val sumbool_not : bool -> bool val dcompare_inf : relation -> bool option val zcompare_rec : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 val z_eq_dec : z -> z -> bool val z_lt_dec : z -> z -> bool val z_gt_dec : z -> z -> bool val z_ge_dec : z -> z -> bool val z_lt_ge_dec : z -> z -> bool val z_gt_le_dec : z -> z -> bool val z_ge_lt_dec : z -> z -> bool module Raw : functor (X:OrderedType) -> sig module E : sig type t = X.t val compare : t -> t -> t compare end module ME : sig val eq_dec : X.t -> X.t -> bool val lt_dec : X.t -> X.t -> bool end type elt = E.t type t = elt list val empty : t val is_empty : t -> bool val mem : elt -> t -> bool val add : elt -> t -> t val singleton : elt -> t val remove : elt -> t -> t val union : t -> t -> t val inter : t -> t -> t val diff : t -> t -> t val equal : t -> t -> bool val subset : t -> t -> bool val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 val filter : (elt -> bool) -> t -> t val for_all : (elt -> bool) -> t -> bool val exists : (elt -> bool) -> t -> bool val partition : (elt -> bool) -> t -> (t, t) prod val cardinal : t -> nat val elements : t -> elt list val min_elt : t -> elt option val max_elt : t -> elt option val choose : t -> elt option val compare : t -> t -> t compare end module Make : functor (X:OrderedType) -> sig module E : sig type t = X.t val compare : t -> t -> t compare end module ME : sig val eq_dec : X.t -> X.t -> bool val lt_dec : X.t -> X.t -> bool end type elt = X.t type tree = | Leaf | Node of tree * X.t * tree * z val tree_rect : 'a1 -> (tree -> 'a1 -> X.t -> tree -> 'a1 -> z -> 'a1) -> tree -> 'a1 val tree_rec : 'a1 -> (tree -> 'a1 -> X.t -> tree -> 'a1 -> z -> 'a1) -> tree -> 'a1 val height : tree -> z val max : z -> z -> z type t_ = tree (* singleton inductive, whose constructor was t_intro *) val t__rect : (tree -> __ -> __ -> 'a1) -> t_ -> 'a1 val t__rec : (tree -> __ -> __ -> 'a1) -> t_ -> 'a1 val the_tree : t_ -> tree type t = t_ val t_empty : t val empty : t sig0 val is_empty : t -> bool val mem : elt -> t -> bool val singleton_tree : elt -> tree val singleton : elt -> t sig0 val create : tree -> elt -> tree -> tree sig0 val bal : tree -> elt -> tree -> tree sig0 val add_tree : elt -> tree -> tree sig0 val add : elt -> t -> t sig0 val join : tree -> elt -> tree -> tree sig0 val remove_min : tree -> (tree, elt) prod sig0 val remove_max : tree -> (tree, elt) prod sig0 val merge : tree -> tree -> tree sig0 val merge_bis : tree -> tree -> tree sig0 val remove_tree : elt -> tree -> tree sig0 val remove : elt -> t -> t sig0 val min_elt : t -> elt sig0 option val max_elt : t -> elt sig0 option val choose : t -> elt sig0 option val concat : tree -> tree -> tree sig0 val split : elt -> tree -> (tree, (bool, tree) prod) prod sig0 val inter : t -> t -> t sig0 val diff : t -> t -> t sig0 val elements_tree_aux : X.t list -> tree -> X.t list val elements_tree : tree -> X.t list val elements : t -> elt list sig0 val cardinal_tree : tree -> nat val cardinal : t -> nat sig0 val cardinal_rec2 : (tree -> tree -> (tree -> tree -> __ -> 'a1) -> 'a1) -> tree -> tree -> 'a1 val union : t -> t -> t sig0 val filter_acc : (elt -> bool) -> tree -> tree -> tree sig0 val filter : (elt -> bool) -> t -> t sig0 val partition_acc : (elt -> bool) -> tree -> tree -> tree -> (tree, tree) prod sig0 val partition : (elt -> bool) -> t -> (t, t) prod sig0 val subset : t -> t -> bool val for_all : (elt -> bool) -> t -> bool val exists : (elt -> bool) -> t -> bool module L : sig module E : sig type t = E.t val compare : t -> t -> t compare end module ME : sig val eq_dec : E.t -> E.t -> bool val lt_dec : E.t -> E.t -> bool end type elt = E.t type t = elt list val empty : t val is_empty : t -> bool val mem : elt -> t -> bool val add : elt -> t -> t val singleton : elt -> t val remove : elt -> t -> t val union : t -> t -> t val inter : t -> t -> t val diff : t -> t -> t val equal : t -> t -> bool val subset : t -> t -> bool val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 val filter : (elt -> bool) -> t -> t val for_all : (elt -> bool) -> t -> bool val exists : (elt -> bool) -> t -> bool val partition : (elt -> bool) -> t -> (t, t) prod val cardinal : t -> nat val elements : t -> elt list val min_elt : t -> elt option val max_elt : t -> elt option val choose : t -> elt option val compare : t -> t -> t compare end val fold_tree : (elt -> 'a1 -> 'a1) -> tree -> 'a1 -> 'a1 val fold_tree' : (elt -> 'a1 -> 'a1) -> tree -> 'a1 -> 'a1 val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 sig0 val flatten : tree list -> elt list val measure_t : tree -> z val measure_l : tree list -> z val compare_rec2 : (tree list -> tree list -> (tree list -> tree list -> __ -> 'a1) -> 'a1) -> tree list -> tree list -> 'a1 val compare_aux : tree list -> tree list -> L.t compare val compare : t -> t -> t compare val equal : t -> t -> bool end module Nat : OrderedType module NatAVL : sig module E : sig type t = Nat.t val compare : t -> t -> t compare end module ME : sig val eq_dec : Nat.t -> Nat.t -> bool val lt_dec : Nat.t -> Nat.t -> bool end type elt = Nat.t type tree = | Leaf | Node of tree * Nat.t * tree * z val tree_rect : 'a1 -> (tree -> 'a1 -> Nat.t -> tree -> 'a1 -> z -> 'a1) -> tree -> 'a1 val tree_rec : 'a1 -> (tree -> 'a1 -> Nat.t -> tree -> 'a1 -> z -> 'a1) -> tree -> 'a1 val height : tree -> z val max : z -> z -> z type t_ = tree (* singleton inductive, whose constructor was t_intro *) val t__rect : (tree -> __ -> __ -> 'a1) -> t_ -> 'a1 val t__rec : (tree -> __ -> __ -> 'a1) -> t_ -> 'a1 val the_tree : t_ -> tree type t = t_ val t_empty : t val empty : t sig0 val is_empty : t -> bool val mem : elt -> t -> bool val singleton_tree : elt -> tree val singleton : elt -> t sig0 val create : tree -> elt -> tree -> tree sig0 val bal : tree -> elt -> tree -> tree sig0 val add_tree : elt -> tree -> tree sig0 val add : elt -> t -> t sig0 val join : tree -> elt -> tree -> tree sig0 val remove_min : tree -> (tree, elt) prod sig0 val remove_max : tree -> (tree, elt) prod sig0 val merge : tree -> tree -> tree sig0 val merge_bis : tree -> tree -> tree sig0 val remove_tree : elt -> tree -> tree sig0 val remove : elt -> t -> t sig0 val min_elt : t -> elt sig0 option val max_elt : t -> elt sig0 option val choose : t -> elt sig0 option val concat : tree -> tree -> tree sig0 val split : elt -> tree -> (tree, (bool, tree) prod) prod sig0 val inter : t -> t -> t sig0 val diff : t -> t -> t sig0 val elements_tree_aux : Nat.t list -> tree -> Nat.t list val elements_tree : tree -> Nat.t list val elements : t -> elt list sig0 val cardinal_tree : tree -> nat val cardinal : t -> nat sig0 val cardinal_rec2 : (tree -> tree -> (tree -> tree -> __ -> 'a1) -> 'a1) -> tree -> tree -> 'a1 val union : t -> t -> t sig0 val filter_acc : (elt -> bool) -> tree -> tree -> tree sig0 val filter : (elt -> bool) -> t -> t sig0 val partition_acc : (elt -> bool) -> tree -> tree -> tree -> (tree, tree) prod sig0 val partition : (elt -> bool) -> t -> (t, t) prod sig0 val subset : t -> t -> bool val for_all : (elt -> bool) -> t -> bool val exists : (elt -> bool) -> t -> bool module L : sig module E : sig type t = E.t val compare : t -> t -> t compare end module ME : sig val eq_dec : E.t -> E.t -> bool val lt_dec : E.t -> E.t -> bool end type elt = E.t type t = elt list val empty : t val is_empty : t -> bool val mem : elt -> t -> bool val add : elt -> t -> t val singleton : elt -> t val remove : elt -> t -> t val union : t -> t -> t val inter : t -> t -> t val diff : t -> t -> t val equal : t -> t -> bool val subset : t -> t -> bool val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 val filter : (elt -> bool) -> t -> t val for_all : (elt -> bool) -> t -> bool val exists : (elt -> bool) -> t -> bool val partition : (elt -> bool) -> t -> (t, t) prod val cardinal : t -> nat val elements : t -> elt list val min_elt : t -> elt option val max_elt : t -> elt option val choose : t -> elt option val compare : t -> t -> t compare end val fold_tree : (elt -> 'a1 -> 'a1) -> tree -> 'a1 -> 'a1 val fold_tree' : (elt -> 'a1 -> 'a1) -> tree -> 'a1 -> 'a1 val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 sig0 val flatten : tree list -> elt list val measure_t : tree -> z val measure_l : tree list -> z val compare_rec2 : (tree list -> tree list -> (tree list -> tree list -> __ -> 'a1) -> 'a1) -> tree list -> tree list -> 'a1 val compare_aux : tree list -> tree list -> L.t compare val compare : t -> t -> t compare val equal : t -> t -> bool end