Skip to content
Snippets Groups Projects
Select Git revision
  • ci-release protected
  • ci/msammler/more_feed
  • ci/refactor_staging
  • coq-stdpp-1.0 protected
  • dfrumin/coq-stdpp-set_map_2
  • master default protected
  • msammler/bitvector
  • msammler/bool_decide_simpl_never
  • msammler/monad_without_universe_constraints
  • ralf/empty-opaque
  • ralf/hint-mode-check
  • ralf/hint-mode-plus
  • ralf/listZ
  • ralf/lookup_insert
  • ralf/make_simple_intropattern
  • ralf/multiset-solver
  • robbert/cancel_inj_surj
  • robbert/cbn
  • robbert/f_equiv_pointwise
  • robbert/from_option
  • coq-stdpp-1.11.0 protected
  • coq-stdpp-1.10.0 protected
  • coq-stdpp-1.9.0 protected
  • coq-stdpp-1.8.0 protected
  • coq-stdpp-1.7.0 protected
  • coq-stdpp-1.6.0 protected
  • coq-stdpp-1.5.0 protected
  • coq-stdpp-1.4.0 protected
  • coq-stdpp-1.3.0 protected
  • coq-stdpp-1.2.1 protected
  • coq-stdpp-1.2.0 protected
  • coq-stdpp-1.1.0 protected
  • coq-stdpp-1.0.0 protected
33 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.04Feb331Jan9Dec86529Nov2423222120191817161510727Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb2625242322212019171615141311109842127Jan222018161412422Dec2115118420Nov19181716113Feb110Jun5221May22Apr1615Mar225Feb2416138130Jan29272523Dec181623Nov1569Oct86230Sep251613126326Aug22976410Jul425Jun23171676524May22429Sep27Aug2115141224Jun1721May15121172Apr25Mar1424Feb221919Jan512Nov19Oct104Sep30Aug29242121Jun1411Add 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.More multiset stuff.Fix typo.Merge branch 'nclose_subseteq' into 'master' Some tweaks to minimal.Make some arguments explicit that could not be infered.More set_Forall and set_Exists stuff for finite sets.