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.07Feb64331Jan9Dec86529Nov2423222120191817161510727Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb2625242322212019171615141311109842127Jan222018161412422Dec2115118420Nov19181716113Feb110Jun5221May22Apr1615Mar225Feb2416138130Jan29272523Dec181623Nov1569Oct86230Sep251613126326Aug22976410Jul425Jun23171676524May22429Sep27Aug2115141224Jun1721May15121172Apr25Mar1424Feb221919Jan512Nov19Oct104Sep30Aug29242121Jun1411update build system, CI and READMEAlso support Coq 8.5pl3.Fix typo.Move COQ FLAGS to _CoqProject.Make f_equiv stronger.add opam and CI stuff (with preliminary names)Add README.Add makefiles and license.A bunch of missing Params instances.Operations for converting between maps and collections.Curry and uncurry operations on gmap.Fold operation on finite maps.Bump year in prelude copyright headers.Vector tweaks.Use primitive projections for sealingMake instances EqDecision and Countable of gmultiset less eager.Recursive [inv_vec].Renaming in prelude/list.more restrictive Proof Using hints in (most files of the) preludeTweak some proof using tweaks for setoid stuff.tune "Proof using" directives to minimize differences to previous types of all lemmasdon't use Proof Using in a few files that get too many unnecessary annotations from thisRequire `Total R` just for the merge sort theorems that actually need it.Document list_remove and list_remove_list.Fix more _L lemmas.make "make quick" quick by adding hints about the used section variablesadd decide_left, decide_rightMove stuff out of sections that does not depend on the section variables.Simplify proofs relating nth to lookup.list: relate nth and lookupA few lemmas about vec and fin.Rename fmap_Some_equiv' → fmap_Some_equiv_1.rename _setoid suffix to _equiv; add variant of fmap_Some_setoid that can be usefully destructedFix breaking ee6df099.Optimize simplify_eq.Avoid exponential blowup in [done] as caused by a7e91677.fix compatibility with latest Coq 8.6Factor out some common properties about lists.New definition of contractive.Some more of_list stuff.