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
  • ralf/no-notypeclasses-apply
  • 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.018Feb17141311130Jan181716151319Dec622Nov2111762131Oct7119Sep1211529Aug27262423151413713Jul98754330Jun2827262521201814230May26252117151210984330Apr262524231926Mar161514643128Feb2322212017131076129Jan28252419131119Dec1615141230Nov28262220121110984115Oct7430Sep181Aug23Jul171030Jun292825232120181410976530May2928242314927Apr2421181110965328Mar2722218623Feb22211916151312983231Jan25231413121019Dec181785429Nov282221201816121193131Oct2827242019181716131097629Sep28272624212019181786222Aug17825Jul26Jun30May251Apr20Mar171615141198123Feb221916151413109764331JanMerge branch 'robbert/top_set' into 'master'CHANGELOG entry.`TopSet` instance for `boolset`.Add class `TopSet` for sets with ⊤ element.Move lattice related stuff up.Remove obsolete `Hint Extern`s that predate the `Hint Mode` declarations.`Prop` is inhabited.Merge branch 'z-greater-decidability' into 'master'Add decidability instances for Z.gt and Z.gedrop 8.9 timing againtemporarily also time 8.9.1 againenable docs againrely on default timing conf nametime on 8.11 instead of 8.10Merge branch 'lookup_total' into 'master'Fix the notation for LookupTotaltest 8.11.0 releaseMerge branch 'tcforall2_forall' into 'master'added tcforall2_forall lemmaAdd lemma `binder_delete_empty`.Add lemma `map_lookup_zip_with_Some`.Add `map_zip_with_proper`.`Proper` instances for HO-functions on lists.Add lemma `lookup_zip_with_Some`.Strengten `fmap_equiv_ext` lemmas.Some generic results on binders that were in Iris.Lemma for lookup of cons.fix READMEstop timing Coq masterfix opam version numberdisable docs building for now, SSH login is brokenopam 2 upgradetemporarily time Coq masterbump to Coq 8.10.2Coq 8.11 is fixedallow 8.11 job to fail while we investigatemake opam dependency more tightly match what we testtest the Coq 8.11 branchMerge branch 'opaquify-gmap' into 'master'Opaquify proofs in gmap_partial_alter (fix #46)