Skip to content
Snippets Groups Projects
Select Git revision
  • ascii-sections
  • basic-dune
  • bi_pure_scopes
  • doc-equalities
  • explicit-vdash
  • fix-497-hint-immediate
  • fix-notation
  • fupd-commutes
  • inv_exc_0_ipm
  • later-credits-drop
  • later_impl_experiments
  • later_impl_test
  • master default
  • more-convenient-fupd_proper
  • no-bi-canonical
  • notations
  • paolo/tc-strict-resolution-backport
  • periscopes
  • periscopes-v2
  • seal_ires
  • iris-4.3.0
  • iris-4.2.0
  • iris-4.1.0
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • iris-3.2.0
  • iris-3.1.0
  • iris-3.0.0
  • iris-2.0
  • iris-2.0-rc2
  • iris-2.0-rc1
  • iris-1.1
  • iris-1.0
  • hope-2015-coq-1
  • appendix-1.0.0
  • appendix-1
39 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.025Sep2421201918171598628Aug26242322201776428Jul14121027Jun13128625May1712927Apr261913121175431Mar30282423222120161514121110976124Feb2322212018171615141312111097632130Jan2928272625242322212017131211109876543128Dec2726232221201918161514131211987652130Nov292827262524232221Add a `repeat (wp_pure _)` example.The `PureExec` typeclass for performing pure symbolic executions.Version of wp_bind_inv for ectx languages.Merge branch 'unit' into 'master'Steps are preserved by permutations.Hacky way of dealing with `iSpecialize ("H" !$ x)` where `x` contains TC holes.update for Coq Makefile hooksfix Makefile; fix coq-stdpp depBump stdpp.fix MakefileA stronger induction principle for fixpoints.Make sure that the fixpoints are non-expansive.Prove `LanguageCtx Λ id`.fix opamtry to fix opamtry to fix opamtry to fix opamBump coqstdpp.add back opam.pins temporarily to unbreak Coq's CIopam: remove redundant parenthesesMakefile tweaksupdate READMECI: tweaksmake build-dep: handle case where the pin already existsMerge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqnew build-dep handling without opam.pinsRename fix.v → fixpoint.v because fix is a reserved keyword.Use a type class for monotone uPred predicates.Show that heap_lang expressions are countable.CI: depend on std++ via opam; prepare for automatic opam releasesGet rid of TimelessL and PersistentL and use TCForall instead.Use ε for CMRA unit.Fix previous commit.Update to latest stdpp, and set Hint Mode of classes.Merge branch 'master' into 'master'Set notation scopes of some language stuff.Printing boxes and breaking points for WP.Some notation tweaking.Bump coq-std++.Bump coq-stdpp.
Loading