opam package, see : https://coq.inria.fr/opam-packaging.html https://github.com/coq-community/manifesto extra ops filter + partition + for_all + exists singleton split ? min_binding, max_binding, choose ? remove_min, remove_max ? update (The one of OCaml, mixing find + add/remove) gmerge (as already in AVL) ? unsure mapo (from AVL and RBT) ? common merge instance, such as diff, inter, union ? Cf Facts of_list = fold add, of_sorted_list (cf treeify in RBT) ? add_cardinal_2 (cf PR Coq) SameKeys another equivalence on maps (on keys only) –> here named Eqdom short filenames (MMap.Interface au lieu de MMapInterface) improve demo.v Why ZM.Raw.key appears in Print map3 : “Definition key” was too early in Raw.Pack do we want ZM.key or Z ? How to choose ? Weird : R.key becomes Z, not ZM.key ?! R.empty without implicit elt ? type of Mkt ? test demo.v and Coq 8.11 avoid printing message during compilation ? Maps on unit + Eqdom –> an MSets implementation Issue : compare on sets ? : dilute Sord inside S, with a compare taking a elt_compare as argument ? improve generic implem in AVL, RBT improve generic implem in Positive args order in equal_spec vs. compare_spec facts : from compare_spec to compare_sym, compare_trans, StrictOrder, etc Maps as OrderedTypes ? fix weird specs like merge_spec1 (?) unified spec of add and remove based on some key_eqb (cf. add_o) ? Not ideal since DecidableType K have K.eq_dec, not K.eqb AVL.gmerge could start by comparing height (better have the little map on the right) RBT could have ins_below, join, split, and merge via split+join ? check complexity in this case ? module AVLproofs with AVL invariant proofs module RBTproofs with RedBlack invariant proofs Interface Raw and module Raw.Pack Btw : why no need for apply ok in Raw.Pack.bindings_spec2 ??!! provide a MultiSets.v (and update it), cf Fset contrib document the expected complexities test extraction Reorganisation GenTree better name for the T module put MapsTo just after, instead of at the very end of (AVL/RBT).MakeRaw directly use In0 instead of two version (inductive vs exists) ? warnings in Coq 8.11 Hints not in core