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.014Mar1198123Feb221916151413109764331Jan9Dec86529Nov2423222120191817161510727Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb2625242322212019171615141311109842127Jan222018161412422Dec2115118420Nov19181716113Feb110Jun5221May22Apr1615Mar225Feb2416138130Jan29272523Dec181623Nov1569Oct86230Sep251613126326Aug22976410Jul425Jun23171676524May22429Sep27Aug2115141224Jun1721May15121172Apr25Mar1424Feb221919Jan512Nov19Oct104Sep30Aug29242121Jun1411prove rtc_subrelMisc numbers stuff.Rename preserving -> mono.Mononicity of ∖.Prove nat_iter_ind.Blacklist `_obligation_` for Search.Add conditional `done` tactic.speed up f_equiv by doing reflexivity less oftenPartially revert "add target html and gallinahtml"Remove some notations that are already in the Coq stdlib.use new CI machinesolve_proper: Do not enforce unfolding the head symbolMerge branch 'benoit/coq-stdpp-make_html'More 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.