package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2025.06.1.tar.bz2
sha256=e92b42fa69da7c730b0c26dacf842a72b4febcaf4f2157a1dc18b3cce1f859fa
doc/jasmin.jasmin/Jasmin/FMapAVL/Make/Raw/Proofs/index.html
Module Raw.Proofs
module MX : sig ... endmodule PX : sig ... endmodule L : sig ... endval coq_R_mem_rect :
X.t ->
('a1 tree -> __ -> 'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
bool ->
'a1 coq_R_mem ->
'a2 ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
bool ->
'a1 coq_R_mem ->
'a2 ->
'a2) ->
'a1 tree ->
bool ->
'a1 coq_R_mem ->
'a2val coq_R_mem_rec :
X.t ->
('a1 tree -> __ -> 'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
bool ->
'a1 coq_R_mem ->
'a2 ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
bool ->
'a1 coq_R_mem ->
'a2 ->
'a2) ->
'a1 tree ->
bool ->
'a1 coq_R_mem ->
'a2type 'elt coq_R_find = | R_find_0 of 'elt tree| R_find_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'elt option * 'elt coq_R_find| R_find_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t| R_find_3 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'elt option * 'elt coq_R_find
val coq_R_find_rect :
X.t ->
('a1 tree -> __ -> 'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 option ->
'a1 coq_R_find ->
'a2 ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 option ->
'a1 coq_R_find ->
'a2 ->
'a2) ->
'a1 tree ->
'a1 option ->
'a1 coq_R_find ->
'a2val coq_R_find_rec :
X.t ->
('a1 tree -> __ -> 'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 option ->
'a1 coq_R_find ->
'a2 ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 option ->
'a1 coq_R_find ->
'a2 ->
'a2) ->
'a1 tree ->
'a1 option ->
'a1 coq_R_find ->
'a2type 'elt coq_R_bal = | R_bal_0 of 'elt tree * key * 'elt * 'elt tree| R_bal_1 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t| R_bal_2 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t| R_bal_3 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t| R_bal_4 of 'elt tree * key * 'elt * 'elt tree| R_bal_5 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t| R_bal_6 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t| R_bal_7 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t| R_bal_8 of 'elt tree * key * 'elt * 'elt tree
val coq_R_bal_rect :
('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> 'a2) ->
('a1 tree ->
key ->
'a1 ->
'a1 tree ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
key ->
'a1 ->
'a1 tree ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
key ->
'a1 ->
'a1 tree ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a2) ->
('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> __ -> __ -> 'a2) ->
('a1 tree ->
key ->
'a1 ->
'a1 tree ->
__ ->
__ ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
key ->
'a1 ->
'a1 tree ->
__ ->
__ ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
key ->
'a1 ->
'a1 tree ->
__ ->
__ ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a2) ->
('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> __ -> 'a2) ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
'a1 tree ->
'a1 coq_R_bal ->
'a2val coq_R_bal_rec :
('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> 'a2) ->
('a1 tree ->
key ->
'a1 ->
'a1 tree ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
key ->
'a1 ->
'a1 tree ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
key ->
'a1 ->
'a1 tree ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a2) ->
('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> __ -> __ -> 'a2) ->
('a1 tree ->
key ->
'a1 ->
'a1 tree ->
__ ->
__ ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
key ->
'a1 ->
'a1 tree ->
__ ->
__ ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
key ->
'a1 ->
'a1 tree ->
__ ->
__ ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a2) ->
('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> __ -> 'a2) ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
'a1 tree ->
'a1 coq_R_bal ->
'a2type 'elt coq_R_add = | R_add_0 of 'elt tree| R_add_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'elt tree * 'elt coq_R_add| R_add_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t| R_add_3 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'elt tree * 'elt coq_R_add
val coq_R_add_rect :
key ->
'a1 ->
('a1 tree -> __ -> 'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 tree ->
'a1 coq_R_add ->
'a2 ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 tree ->
'a1 coq_R_add ->
'a2 ->
'a2) ->
'a1 tree ->
'a1 tree ->
'a1 coq_R_add ->
'a2val coq_R_add_rec :
key ->
'a1 ->
('a1 tree -> __ -> 'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 tree ->
'a1 coq_R_add ->
'a2 ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 tree ->
'a1 coq_R_add ->
'a2 ->
'a2) ->
'a1 tree ->
'a1 tree ->
'a1 coq_R_add ->
'a2val coq_R_remove_min_rect :
('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> 'a2) ->
('a1 tree ->
key ->
'a1 ->
'a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
('a1 tree * (key * 'a1)) ->
'a1 coq_R_remove_min ->
'a2 ->
'a1 tree ->
(key * 'a1) ->
__ ->
'a2) ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
('a1 tree * (key * 'a1)) ->
'a1 coq_R_remove_min ->
'a2val coq_R_remove_min_rec :
('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> 'a2) ->
('a1 tree ->
key ->
'a1 ->
'a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
('a1 tree * (key * 'a1)) ->
'a1 coq_R_remove_min ->
'a2 ->
'a1 tree ->
(key * 'a1) ->
__ ->
'a2) ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
('a1 tree * (key * 'a1)) ->
'a1 coq_R_remove_min ->
'a2type 'elt coq_R_merge = | R_merge_0 of 'elt tree * 'elt tree| R_merge_1 of 'elt tree * 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t| R_merge_2 of 'elt tree * 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'elt tree * key * 'elt * key * 'elt
val coq_R_merge_rect :
('a1 tree -> 'a1 tree -> __ -> 'a2) ->
('a1 tree ->
'a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a1 tree ->
(key * 'a1) ->
__ ->
key ->
'a1 ->
__ ->
'a2) ->
'a1 tree ->
'a1 tree ->
'a1 tree ->
'a1 coq_R_merge ->
'a2val coq_R_merge_rec :
('a1 tree -> 'a1 tree -> __ -> 'a2) ->
('a1 tree ->
'a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a1 tree ->
(key * 'a1) ->
__ ->
key ->
'a1 ->
__ ->
'a2) ->
'a1 tree ->
'a1 tree ->
'a1 tree ->
'a1 coq_R_merge ->
'a2type 'elt coq_R_remove = | R_remove_0 of 'elt tree| R_remove_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'elt tree * 'elt coq_R_remove| R_remove_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t| R_remove_3 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'elt tree * 'elt coq_R_remove
val coq_R_remove_rect :
X.t ->
('a1 tree -> __ -> 'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 tree ->
'a1 coq_R_remove ->
'a2 ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 tree ->
'a1 coq_R_remove ->
'a2 ->
'a2) ->
'a1 tree ->
'a1 tree ->
'a1 coq_R_remove ->
'a2val coq_R_remove_rec :
X.t ->
('a1 tree -> __ -> 'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 tree ->
'a1 coq_R_remove ->
'a2 ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 tree ->
'a1 coq_R_remove ->
'a2 ->
'a2) ->
'a1 tree ->
'a1 tree ->
'a1 coq_R_remove ->
'a2val coq_R_concat_rect :
('a1 tree -> 'a1 tree -> __ -> 'a2) ->
('a1 tree ->
'a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a1 tree ->
(key * 'a1) ->
__ ->
'a2) ->
'a1 tree ->
'a1 tree ->
'a1 tree ->
'a1 coq_R_concat ->
'a2val coq_R_concat_rec :
('a1 tree -> 'a1 tree -> __ -> 'a2) ->
('a1 tree ->
'a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a1 tree ->
(key * 'a1) ->
__ ->
'a2) ->
'a1 tree ->
'a1 tree ->
'a1 tree ->
'a1 coq_R_concat ->
'a2type 'elt coq_R_split = | R_split_0 of 'elt tree| R_split_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'elt triple * 'elt coq_R_split * 'elt tree * 'elt option * 'elt tree| R_split_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t| R_split_3 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'elt triple * 'elt coq_R_split * 'elt tree * 'elt option * 'elt tree
val coq_R_split_rect :
X.t ->
('a1 tree -> __ -> 'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 triple ->
'a1 coq_R_split ->
'a2 ->
'a1 tree ->
'a1 option ->
'a1 tree ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 triple ->
'a1 coq_R_split ->
'a2 ->
'a1 tree ->
'a1 option ->
'a1 tree ->
__ ->
'a2) ->
'a1 tree ->
'a1 triple ->
'a1 coq_R_split ->
'a2val coq_R_split_rec :
X.t ->
('a1 tree -> __ -> 'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 triple ->
'a1 coq_R_split ->
'a2 ->
'a1 tree ->
'a1 option ->
'a1 tree ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a2) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
__ ->
'a1 triple ->
'a1 coq_R_split ->
'a2 ->
'a1 tree ->
'a1 option ->
'a1 tree ->
__ ->
'a2) ->
'a1 tree ->
'a1 triple ->
'a1 coq_R_split ->
'a2type ('elt, 'x) coq_R_map_option = | R_map_option_0 of 'elt tree| R_map_option_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'x * 'x tree * ('elt, 'x) coq_R_map_option * 'x tree * ('elt, 'x) coq_R_map_option| R_map_option_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'x tree * ('elt, 'x) coq_R_map_option * 'x tree * ('elt, 'x) coq_R_map_option
val coq_R_map_option_rect :
(key -> 'a1 -> 'a2 option) ->
('a1 tree -> __ -> 'a3) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a2 ->
__ ->
'a2 tree ->
('a1, 'a2) coq_R_map_option ->
'a3 ->
'a2 tree ->
('a1, 'a2) coq_R_map_option ->
'a3 ->
'a3) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
'a2 tree ->
('a1, 'a2) coq_R_map_option ->
'a3 ->
'a2 tree ->
('a1, 'a2) coq_R_map_option ->
'a3 ->
'a3) ->
'a1 tree ->
'a2 tree ->
('a1, 'a2) coq_R_map_option ->
'a3val coq_R_map_option_rec :
(key -> 'a1 -> 'a2 option) ->
('a1 tree -> __ -> 'a3) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a2 ->
__ ->
'a2 tree ->
('a1, 'a2) coq_R_map_option ->
'a3 ->
'a2 tree ->
('a1, 'a2) coq_R_map_option ->
'a3 ->
'a3) ->
('a1 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
'a2 tree ->
('a1, 'a2) coq_R_map_option ->
'a3 ->
'a2 tree ->
('a1, 'a2) coq_R_map_option ->
'a3 ->
'a3) ->
'a1 tree ->
'a2 tree ->
('a1, 'a2) coq_R_map_option ->
'a3type ('elt, 'x0, 'x) coq_R_map2_opt = | R_map2_opt_0 of 'elt tree * 'x0 tree| R_map2_opt_1 of 'elt tree * 'x0 tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t| R_map2_opt_2 of 'elt tree * 'x0 tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'x0 tree * key * 'x0 * 'x0 tree * Int.Z_as_Int.t * 'x0 tree * 'x0 option * 'x0 tree * 'x * 'x tree * ('elt, 'x0, 'x) coq_R_map2_opt * 'x tree * ('elt, 'x0, 'x) coq_R_map2_opt| R_map2_opt_3 of 'elt tree * 'x0 tree * 'elt tree * key * 'elt * 'elt tree * Int.Z_as_Int.t * 'x0 tree * key * 'x0 * 'x0 tree * Int.Z_as_Int.t * 'x0 tree * 'x0 option * 'x0 tree * 'x tree * ('elt, 'x0, 'x) coq_R_map2_opt * 'x tree * ('elt, 'x0, 'x) coq_R_map2_opt
val coq_R_map2_opt_rect :
(key -> 'a1 -> 'a2 option -> 'a3 option) ->
('a1 tree -> 'a3 tree) ->
('a2 tree -> 'a3 tree) ->
('a1 tree -> 'a2 tree -> __ -> 'a4) ->
('a1 tree ->
'a2 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
'a4) ->
('a1 tree ->
'a2 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a2 tree ->
key ->
'a2 ->
'a2 tree ->
Int.Z_as_Int.t ->
__ ->
'a2 tree ->
'a2 option ->
'a2 tree ->
__ ->
'a3 ->
__ ->
'a3 tree ->
('a1, 'a2, 'a3) coq_R_map2_opt ->
'a4 ->
'a3 tree ->
('a1, 'a2, 'a3) coq_R_map2_opt ->
'a4 ->
'a4) ->
('a1 tree ->
'a2 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a2 tree ->
key ->
'a2 ->
'a2 tree ->
Int.Z_as_Int.t ->
__ ->
'a2 tree ->
'a2 option ->
'a2 tree ->
__ ->
__ ->
'a3 tree ->
('a1, 'a2, 'a3) coq_R_map2_opt ->
'a4 ->
'a3 tree ->
('a1, 'a2, 'a3) coq_R_map2_opt ->
'a4 ->
'a4) ->
'a1 tree ->
'a2 tree ->
'a3 tree ->
('a1, 'a2, 'a3) coq_R_map2_opt ->
'a4val coq_R_map2_opt_rec :
(key -> 'a1 -> 'a2 option -> 'a3 option) ->
('a1 tree -> 'a3 tree) ->
('a2 tree -> 'a3 tree) ->
('a1 tree -> 'a2 tree -> __ -> 'a4) ->
('a1 tree ->
'a2 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
__ ->
'a4) ->
('a1 tree ->
'a2 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a2 tree ->
key ->
'a2 ->
'a2 tree ->
Int.Z_as_Int.t ->
__ ->
'a2 tree ->
'a2 option ->
'a2 tree ->
__ ->
'a3 ->
__ ->
'a3 tree ->
('a1, 'a2, 'a3) coq_R_map2_opt ->
'a4 ->
'a3 tree ->
('a1, 'a2, 'a3) coq_R_map2_opt ->
'a4 ->
'a4) ->
('a1 tree ->
'a2 tree ->
'a1 tree ->
key ->
'a1 ->
'a1 tree ->
Int.Z_as_Int.t ->
__ ->
'a2 tree ->
key ->
'a2 ->
'a2 tree ->
Int.Z_as_Int.t ->
__ ->
'a2 tree ->
'a2 option ->
'a2 tree ->
__ ->
__ ->
'a3 tree ->
('a1, 'a2, 'a3) coq_R_map2_opt ->
'a4 ->
'a3 tree ->
('a1, 'a2, 'a3) coq_R_map2_opt ->
'a4 ->
'a4) ->
'a1 tree ->
'a2 tree ->
'a3 tree ->
('a1, 'a2, 'a3) coq_R_map2_opt ->
'a4val flatten_e : 'a1 enumeration -> (key * 'a1) list