Skip to content
Snippets Groups Projects
Select Git revision
  • coq-stdpp-1.0
  • master default protected
  • mraise
  • coq-stdpp-1.8.0
  • coq-stdpp-1.7.0
  • 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
13 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.011Sep65130Aug283229Jul2725212Jun131May30111095432130Apr2825241918141124Mar2120191817817Feb1376419Jan216Dec151312530Nov2925242318171615220Oct8629Sep28272524232120725Aug24231716121110983131Jul272618728Jun2726830May251613119864312Apr11730Mar18161524Feb2022Jan19171413121122Dec211613987632130Nov262423221815131285427Oct2613952127Sep2625131098765454Merge branch 'ralf/fmap_inj' into 'master'mastermasterCHANGELOG typo.CHANGELOG.Tweaks.Add instance `bv_unsigned_inj` and use that.prove a general option_fmap_inj lemma, and a similar one for listsMerge branch 'robbert/string_ascii_countable' into 'master'CHANGELOG.Tweak comments.Comment, rename, make Local.Tweak Ltac generator.Better `decode` for `string` that is generated.Better coding for string/ascii.Add missing `Local` in `pmap`.Merge branch 'bv-notations' into 'master'Add bitvector number notationsMerge branch 'ralf/ge' into 'master'improve commentAdd MRaise typeclassmraisemraiseexplain why we don't have 'ge' notationMerge branch 'ike/hint_mode_leibniz_equiv' into 'master'Change Hint Mode of LeibnizEquivmore comment tweaks (by Robbert)Merge branch 'ralf/multiset-solver' into 'master'more precise commentuse ssreflect rewrite for multiset tacticsMerge branch 'fold_comm_acc_lemmas' into 'master'Ralf's suggestions.Tweak proofs.Add fold-commuting lemmas to CHANGELOG.mdWeaken premises and tweak proofs.Rename comm_acc -> comm_accumStrengthen all fold commutativity lemmasStrengthen multiset disj union lemmaExtend fold-commuting lemmas to lists, setsAdd lemmas for commuting funcs with foldsMerge branch 'robbert/params_lookup' into 'master'Add CHANGELOG.Correct `Params` instances for `lookup` and `singletonM`.Merge branch 'ralf/pair_equiv' into 'master'