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/list-module
  • ralf/listZ
  • ralf/lookup_insert
  • ralf/make_simple_intropattern
  • ralf/multiset-solver
  • robbert/cancel_inj_surj
  • robbert/cbn
  • robbert/f_equiv_pointwise
  • 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.011Jan19Dec1615141230Nov28262220121110984115Oct7430Sep181Aug23Jul171030Jun292825232120181410976530May2928242314927Apr2421181110965328Mar2722218623Feb22211916151312983231Jan25231413121019Dec181785429Nov282221201816121193131Oct2827242019181716131097629Sep28272624212019181786222Aug17825Jul26Jun30May251Apr20Mar171615141198123Feb221916151413109764331Jan9Dec86529Nov2423222120191817161510727Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb2625242322212019171615141311109842127Jan222018161412422Dec2115118420Nov19`tc_to_bool P` to turn a type class into a Boolean that represents if there is an instance.update CI configMerge branch 'map_filter_lemmata' into 'master'Add results about deleting and inserting filtered out elementsMerge branch 'master' into 'master'Get rid of the awk.Makefile referencesInline equality premise in `map_insert_zip_with`.Show that accessible elements do not loop.Bit of clean up.Type class version of `elem_of` for lists.Merge branch 'add_docs_to_readme' into 'master'Merge branch 'no-implicit-core' into 'master'Explicitly use core hint databaseVersions of `elem_of_list_split` that give first or last element.reorder some files for better coqdocAdd link to docs to the Readmeself-compiled ocaml is the new defaultI meant all the timing jobscompile our own ocaml so that opam doesn't act up the way it usually likes toProve map_Forall_delete.More results about filter on map.Lemma prefix_lookup.Add `Nat_iter_add`.remove no-longer-needed Makefile hackeryDrop support for Coq 8.6.Merge branch 'robbert/simpl_Z' into 'master'Consistently block `simpl` on all `Z` operations.Support singletons in `solve_map_disjoint`.also declare compatibility with Coq 8.9 in opam filealso test 8.9 development branchsupport Coq 8.8.2Add `collection_map` and some basic theory about it.UI tests actually work for current Coquse newer ocaml for Coq masteruse Docker image matching CI branchautoamtically use latest CIfix CIupdate CI for opam 2WIP CIupdate CI
Loading