Skip to content
Snippets Groups Projects
Select Git revision
  • coq-stdpp-1.0
  • glen/finite-nodec
  • master default protected
  • msammler/bitvector
  • msammler/bool_decide_simpl_never
  • ralf/hint-mode-check
  • robbert/cbn
  • robbert/f_equiv_pointwise
  • robbert/from_option
  • robbert/map_filter_True_False
  • robbert/multiset_singleton
  • robbert/tc_opaque
  • tchajed/stdpp-sprop-gmap
  • coq-stdpp-1.6.0
  • 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
21 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.019Feb16151413109764331Jan9Dec86529Nov2423222120191817161510727Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb2625242322212019171615141311109842127Jan222018161412422Dec2115118420Nov19181716113Feb110Jun5221May22Apr1615Mar225Feb2416138130Jan29272523Dec181623Nov1569Oct86230Sep251613126326Aug22976410Jul425Jun23171676524May22429Sep27Aug2115141224Jun1721May15121172Apr25Mar1424Feb221919Jan512Nov19Oct104Sep30Aug29242121Jun1411More consistent notations for curried relations.record timing information in artifactRename set_Forall_weaken → set_Forall_impl.Add a variant of lookup_insert_is_Some.Lemma for X ∪ Y ⊆ Z ↔ X ⊆ Z ∧ Y ⊆ Z.add target html and gallinahtmlopam: fix uninstallcoq-stdpp-1.0coq-stdpp-1.0add homepage to opam fileedit opam filecoq-stdpp-1.0.0coq-stdpp-1.0.0Add a contributor's guideMake arguments for sig and sigT constructors and projections maximally implicit.Prove elem_of_submseteq.Propers for monadic operations on option.Merge branch 'ralf/buildsys' into 'master' update 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 variables