Skip to content
Snippets Groups Projects
Select Git revision
  • coq-stdpp-1.0
  • hai/more_finmaps
  • master default protected
  • msammler/bitvector
  • msammler/little_endian
  • robbert/cbn
  • robbert/from_option
  • robbert/multiset_singleton
  • robbert/tc_opaque
  • coq-stdpp-1.5.0
  • coq-stdpp-1.4.0
  • coq-stdpp-1.3.0
  • coq-stdpp-1.2.1
  • coq-stdpp-1.2.0
  • coq-stdpp-1.1.0
  • coq-stdpp-1.0.0
16 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.019Aug17842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb2625242322212019171615141311109842127Jan222018161412422Dec2115118420Nov19181716113Feb110Jun5221May22Apr1615Mar225Feb2416138130Jan29272523Dec181623Nov1569Oct86230Sep251613126326Aug22976410Jul425Jun23171676524May22429Sep27Aug2115141224Jun1721May15121172Apr25Mar1424Feb221919Jan512Nov19Oct104Sep30Aug29242121Jun1411make coqchk happy with prelude.prettyMake coqchk slightly happier with prelude/prettyMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqInhabited instance for any Empty instance.Better Coq 8.6 compatibilitySome general stuff about fin.Injectivity instance for Z.of_nat.Unfolding properties for Nat.iter.Sets of sequences of natural numbers.Conversion from coPset to gset positive.Make hlist universe polymorphic.Revert "Make the types of the finite map type classes more specific."Make the types of the finite map type classes more specific.Relate subseteq on collections to the extension order.More documentation of [coPset].Forgot to commit prelude/sorting, this fixes 6dbe0c27.Version of fresh using an existential.More mapset deciders.More coPset deciders.Move sorting stuff to separate file.Simplify collection spaghetti.Remove unused set_NoDup stuff.Improve organization of prelude/fin_collections.Remove some generic decision procedures for sets.More consistent file names for coPset, bset and set.Make ∖ left associative.Turn unused disjoint_union_difference into something more sensible.LeibnizEquiv instance for unit.Remove CollectionOps class.Rename fallthrough (instances) into default.Notation for max and min.Qp is inhabited.Use ndot_ne_disjoint more eager so it expands definitions.Make Program obligations Transparent by default.New lemma aboud maps : fmap_deleteHack to avoid getting String.length instead of List.length.Some properties of imapImprove solve_proper a bit.More hlist stuff.More heterogeneous list stuff.