type __ = Obj.t type nat = | O | S of nat type ('a, 'b) sum = | Inl of 'a | Inr of 'b type ('a, 'b) prod = | Pair of 'a * 'b val fst : ('a1, 'a2) prod -> 'a1 val snd : ('a1, 'a2) prod -> 'a2 type 'a sig0 = 'a (* singleton inductive, whose constructor was exist *) type 'a list = | Nil | Cons of 'a * 'a list type 'x compare = | Lt | Eq | Gt module type OrderedType = sig type t val compare : t -> t -> t compare end module type S = sig module E : OrderedType type elt = E.t type t 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 compare : t -> t -> t compare val equal : t -> t -> bool val subset : t -> t -> bool val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 val for_all : (elt -> bool) -> t -> bool val exists : (elt -> bool) -> t -> bool val filter : (elt -> bool) -> t -> t 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 end module MoreOrderedType : functor (O:OrderedType) -> sig val eq_dec : O.t -> O.t -> bool val lt_dec : O.t -> O.t -> bool end module DepOfNodep : functor (M:S) -> sig module ME : sig val eq_dec : M.E.t -> M.E.t -> bool val lt_dec : M.E.t -> M.E.t -> bool end val empty : M.t sig0 val is_empty : M.t -> bool val mem : M.elt -> M.t -> bool val add : M.elt -> M.t -> M.t sig0 val singleton : M.elt -> M.t sig0 val remove : M.elt -> M.t -> M.t sig0 val union : M.t -> M.t -> M.t sig0 val inter : M.t -> M.t -> M.t sig0 val diff : M.t -> M.t -> M.t sig0 val equal : M.t -> M.t -> bool val subset : M.t -> M.t -> bool val fold : (M.elt -> 'a1 -> 'a1) -> M.t -> 'a1 -> 'a1 sig0 val cardinal : M.t -> nat sig0 val fdec : (M.elt -> bool) -> M.elt -> bool val filter : (M.elt -> bool) -> M.t -> M.t sig0 val for_all : (M.elt -> bool) -> M.t -> bool val exists : (M.elt -> bool) -> M.t -> bool val partition : (M.elt -> bool) -> M.t -> (M.t, M.t) prod sig0 val choose : M.t -> M.elt sig0 option val elements : M.t -> M.elt list sig0 val min_elt : M.t -> M.elt sig0 option val max_elt : M.t -> M.elt sig0 option module E : sig type t = M.E.t val compare : t -> t -> t compare end type elt = M.elt type t = M.t val compare : M.t -> M.t -> M.t compare 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 add0 : 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 zopp : z -> z val zcompare : z -> z -> relation val lt_eq_lt_dec : nat -> nat -> bool option val zs : z -> z val zpred : z -> z val zminus : z -> z -> z 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 zeven_odd_dec : z -> bool val zdiv2_pos : positive -> positive val zdiv2 : z -> z val z_modulo_2 : z -> (z sig0, z sig0) sum val zsplit2 : z -> (z, z) prod sig0 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 Raw : 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 type slist = Raw.t (* singleton inductive, whose constructor was Build_slist *) val slist_rect : (Raw.t -> __ -> 'a1) -> slist -> 'a1 val slist_rec : (Raw.t -> __ -> 'a1) -> slist -> 'a1 val this : slist -> Raw.t type t = slist type elt = X.t val mem : elt -> t -> bool val add : Raw.elt -> slist -> slist val remove : Raw.elt -> slist -> slist val singleton : Raw.elt -> slist val union : t -> t -> slist val inter : t -> t -> slist val diff : t -> t -> slist val equal : t -> t -> bool val subset : t -> t -> bool val empty : slist val is_empty : t -> bool val elements : t -> Raw.elt list val min_elt : t -> Raw.elt option val max_elt : t -> Raw.elt option val choose : t -> Raw.elt option val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 val cardinal : t -> nat val filter : (elt -> bool) -> t -> slist val for_all : (elt -> bool) -> t -> bool val exists : (elt -> bool) -> t -> bool val partition : (elt -> bool) -> t -> (slist, slist) prod val compare : t -> t -> t compare end val zlength_aux : z -> 'a1 list -> z val zlength : 'a1 list -> z val log_inf : positive -> z val n_digits : z -> z module Coq_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 color = | Coq_red | Coq_black val color_rect : 'a1 -> 'a1 -> color -> 'a1 val color_rec : 'a1 -> 'a1 -> color -> 'a1 type tree = | Leaf | Node of color * tree * X.t * tree val tree_rect : 'a1 -> (color -> tree -> 'a1 -> X.t -> tree -> 'a1 -> 'a1) -> tree -> 'a1 val tree_rec : 'a1 -> (color -> tree -> 'a1 -> X.t -> tree -> 'a1 -> 'a1) -> tree -> 'a1 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 type coq_Conflict = | NoConflict | RedRedConflict of tree * tree * tree * elt * elt val coq_Conflict_rect : tree -> (__ -> 'a1) -> (tree -> tree -> tree -> elt -> elt -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> coq_Conflict -> 'a1 val coq_Conflict_rec : tree -> (__ -> 'a1) -> (tree -> tree -> tree -> elt -> elt -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> coq_Conflict -> 'a1 val conflict : tree -> coq_Conflict val lbalance : tree -> elt -> tree -> tree sig0 val rbalance : tree -> elt -> tree -> tree sig0 val insert : elt -> t -> tree sig0 val add : elt -> t -> t sig0 val unbalanced_left : tree -> (tree, bool) prod sig0 val unbalanced_right : tree -> (tree, bool) prod sig0 val remove_min : tree -> (tree, (elt, bool) prod) prod sig0 val blackify : tree -> (tree, bool) prod sig0 val remove_aux : elt -> tree -> (tree, bool) prod sig0 val remove : elt -> t -> t sig0 val of_list_aux_Invariant_rect : z -> z -> elt list -> elt list -> tree -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 val of_list_aux_Invariant_rec : z -> z -> elt list -> elt list -> tree -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 val of_list_aux : z -> z -> elt list -> (tree, elt list) prod sig0 val of_list : elt list -> 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 module Lists : sig module E : sig type t = X.t val compare : t -> t -> t compare end module Raw : 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 type slist = Raw.t (* singleton inductive, whose constructor was Build_slist *) val slist_rect : (Raw.t -> __ -> 'a1) -> slist -> 'a1 val slist_rec : (Raw.t -> __ -> 'a1) -> slist -> 'a1 val this : slist -> Raw.t type t = slist type elt = X.t val mem : elt -> t -> bool val add : Raw.elt -> slist -> slist val remove : Raw.elt -> slist -> slist val singleton : Raw.elt -> slist val union : t -> t -> slist val inter : t -> t -> slist val diff : t -> t -> slist val equal : t -> t -> bool val subset : t -> t -> bool val empty : slist val is_empty : t -> bool val elements : t -> Raw.elt list val min_elt : t -> Raw.elt option val max_elt : t -> Raw.elt option val choose : t -> Raw.elt option val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 val cardinal : t -> nat val filter : (elt -> bool) -> t -> slist val for_all : (elt -> bool) -> t -> bool val exists : (elt -> bool) -> t -> bool val partition : (elt -> bool) -> t -> (slist, slist) prod val compare : t -> t -> t compare end val of_slist : Lists.t -> t sig0 val to_slist : t -> Lists.t sig0 val union : t -> t -> t sig0 val inter : t -> t -> t sig0 val diff : t -> t -> t sig0 val equal : t -> t -> bool val subset : t -> t -> bool 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 cardinal : t -> nat sig0 module DLists : sig module ME : sig val eq_dec : Lists.E.t -> Lists.E.t -> bool val lt_dec : Lists.E.t -> Lists.E.t -> bool end val empty : Lists.t sig0 val is_empty : Lists.t -> bool val mem : Lists.elt -> Lists.t -> bool val add : Lists.elt -> Lists.t -> Lists.t sig0 val singleton : Lists.elt -> Lists.t sig0 val remove : Lists.elt -> Lists.t -> Lists.t sig0 val union : Lists.t -> Lists.t -> Lists.t sig0 val inter : Lists.t -> Lists.t -> Lists.t sig0 val diff : Lists.t -> Lists.t -> Lists.t sig0 val equal : Lists.t -> Lists.t -> bool val subset : Lists.t -> Lists.t -> bool val fold : (Lists.elt -> 'a1 -> 'a1) -> Lists.t -> 'a1 -> 'a1 sig0 val cardinal : Lists.t -> nat sig0 val fdec : (Lists.elt -> bool) -> Lists.elt -> bool val filter : (Lists.elt -> bool) -> Lists.t -> Lists.t sig0 val for_all : (Lists.elt -> bool) -> Lists.t -> bool val exists : (Lists.elt -> bool) -> Lists.t -> bool val partition : (Lists.elt -> bool) -> Lists.t -> (Lists.t, Lists.t) prod sig0 val choose : Lists.t -> Lists.elt sig0 option val elements : Lists.t -> Lists.elt list sig0 val min_elt : Lists.t -> Lists.elt sig0 option val max_elt : Lists.t -> Lists.elt sig0 option module E : sig type t = Lists.E.t val compare : t -> t -> t compare end type elt = Lists.elt type t = Lists.t val compare : Lists.t -> Lists.t -> Lists.t compare end val filter : (elt -> bool) -> t -> t sig0 val for_all : (elt -> bool) -> t -> bool val exists : (elt -> bool) -> t -> bool val partition : (elt -> bool) -> t -> (t, t) prod sig0 val min_elt : t -> elt sig0 option val max_elt : t -> elt sig0 option val choose : t -> elt sig0 option val compare : t -> t -> t compare end module Nat : OrderedType module NatRBT : 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 color = | Coq_red | Coq_black val color_rect : 'a1 -> 'a1 -> color -> 'a1 val color_rec : 'a1 -> 'a1 -> color -> 'a1 type tree = | Leaf | Node of color * tree * Nat.t * tree val tree_rect : 'a1 -> (color -> tree -> 'a1 -> Nat.t -> tree -> 'a1 -> 'a1) -> tree -> 'a1 val tree_rec : 'a1 -> (color -> tree -> 'a1 -> Nat.t -> tree -> 'a1 -> 'a1) -> tree -> 'a1 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 type coq_Conflict = | NoConflict | RedRedConflict of tree * tree * tree * elt * elt val coq_Conflict_rect : tree -> (__ -> 'a1) -> (tree -> tree -> tree -> elt -> elt -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> coq_Conflict -> 'a1 val coq_Conflict_rec : tree -> (__ -> 'a1) -> (tree -> tree -> tree -> elt -> elt -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> coq_Conflict -> 'a1 val conflict : tree -> coq_Conflict val lbalance : tree -> elt -> tree -> tree sig0 val rbalance : tree -> elt -> tree -> tree sig0 val insert : elt -> t -> tree sig0 val add : elt -> t -> t sig0 val unbalanced_left : tree -> (tree, bool) prod sig0 val unbalanced_right : tree -> (tree, bool) prod sig0 val remove_min : tree -> (tree, (elt, bool) prod) prod sig0 val blackify : tree -> (tree, bool) prod sig0 val remove_aux : elt -> tree -> (tree, bool) prod sig0 val remove : elt -> t -> t sig0 val of_list_aux_Invariant_rect : z -> z -> elt list -> elt list -> tree -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 val of_list_aux_Invariant_rec : z -> z -> elt list -> elt list -> tree -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 val of_list_aux : z -> z -> elt list -> (tree, elt list) prod sig0 val of_list : elt list -> 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 module Lists : sig module E : sig type t = Nat.t val compare : t -> t -> t compare end module Raw : 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 = 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 type slist = Raw.t (* singleton inductive, whose constructor was Build_slist *) val slist_rect : (Raw.t -> __ -> 'a1) -> slist -> 'a1 val slist_rec : (Raw.t -> __ -> 'a1) -> slist -> 'a1 val this : slist -> Raw.t type t = slist type elt = Nat.t val mem : elt -> t -> bool val add : Raw.elt -> slist -> slist val remove : Raw.elt -> slist -> slist val singleton : Raw.elt -> slist val union : t -> t -> slist val inter : t -> t -> slist val diff : t -> t -> slist val equal : t -> t -> bool val subset : t -> t -> bool val empty : slist val is_empty : t -> bool val elements : t -> Raw.elt list val min_elt : t -> Raw.elt option val max_elt : t -> Raw.elt option val choose : t -> Raw.elt option val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 val cardinal : t -> nat val filter : (elt -> bool) -> t -> slist val for_all : (elt -> bool) -> t -> bool val exists : (elt -> bool) -> t -> bool val partition : (elt -> bool) -> t -> (slist, slist) prod val compare : t -> t -> t compare end val of_slist : Lists.t -> t sig0 val to_slist : t -> Lists.t sig0 val union : t -> t -> t sig0 val inter : t -> t -> t sig0 val diff : t -> t -> t sig0 val equal : t -> t -> bool val subset : t -> t -> bool 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 cardinal : t -> nat sig0 module DLists : sig module ME : sig val eq_dec : Lists.E.t -> Lists.E.t -> bool val lt_dec : Lists.E.t -> Lists.E.t -> bool end val empty : Lists.t sig0 val is_empty : Lists.t -> bool val mem : Lists.elt -> Lists.t -> bool val add : Lists.elt -> Lists.t -> Lists.t sig0 val singleton : Lists.elt -> Lists.t sig0 val remove : Lists.elt -> Lists.t -> Lists.t sig0 val union : Lists.t -> Lists.t -> Lists.t sig0 val inter : Lists.t -> Lists.t -> Lists.t sig0 val diff : Lists.t -> Lists.t -> Lists.t sig0 val equal : Lists.t -> Lists.t -> bool val subset : Lists.t -> Lists.t -> bool val fold : (Lists.elt -> 'a1 -> 'a1) -> Lists.t -> 'a1 -> 'a1 sig0 val cardinal : Lists.t -> nat sig0 val fdec : (Lists.elt -> bool) -> Lists.elt -> bool val filter : (Lists.elt -> bool) -> Lists.t -> Lists.t sig0 val for_all : (Lists.elt -> bool) -> Lists.t -> bool val exists : (Lists.elt -> bool) -> Lists.t -> bool val partition : (Lists.elt -> bool) -> Lists.t -> (Lists.t, Lists.t) prod sig0 val choose : Lists.t -> Lists.elt sig0 option val elements : Lists.t -> Lists.elt list sig0 val min_elt : Lists.t -> Lists.elt sig0 option val max_elt : Lists.t -> Lists.elt sig0 option module E : sig type t = Lists.E.t val compare : t -> t -> t compare end type elt = Lists.elt type t = Lists.t val compare : Lists.t -> Lists.t -> Lists.t compare end val filter : (elt -> bool) -> t -> t sig0 val for_all : (elt -> bool) -> t -> bool val exists : (elt -> bool) -> t -> bool val partition : (elt -> bool) -> t -> (t, t) prod sig0 val min_elt : t -> elt sig0 option val max_elt : t -> elt sig0 option val choose : t -> elt sig0 option val compare : t -> t -> t compare end