Skip to content
Snippets Groups Projects
Select Git revision
  • ci/3.1.0
  • ci/debug
  • ci/disable-ltac-backtrace
  • ci/for_proph
  • ci/janno/debug-opam
  • ci/janno/let_bind_envs
  • ci/janno/vmcast
  • ci/joe/compact_ipm
  • ci/joe/compact_ipm_remaining
  • ci/joe/compact_ipm_simple
  • ci/maximedenes/instance-nobody-open-proof
  • ci/msammler/iris-coq-seal_big_opM
  • ci/mtac2-tt
  • ci/prophecy
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/ralf/set_unfold_elements
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • 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
31 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.027Nov26232220161211986131Oct292726252422212019181312111075432130Sep27262019181210331Aug3029241713112131Jul242319181713976543230Jun2928262523222120191817161514131211109876543131May302928272524232018171514111098743230Apr29282726252423222120191812111096Fix bug in `wp_cas_suc`.Add `locC`, the OFE on locations.Bump stdpp.Commonly used variant of `singleton_included` when the element is exclusive.Stop requiring prophecy variables to be mapped to Some location in the invariantProof of conditional-counter spec from Turon et al. (2013)Adding support for prophecy resolution to heap_lang.CASMerge branch 'patch-1' into 'master'Link to HTML sources for easier navigationpublish coqdocsself-compiled ocaml is the new defaultOne more occurence...Do not manually apply TC instances using `refine`.Merge branch 'patch-1' into 'master'Update the link to std++Bump std++ once more.Bump Iris.Bump stdpp.Bump Mtac2-8.8 commit to restore Coq 8.8.0 compat.make opam and README reflect realityremove no-longer-needed Makefile hackerybump stdpp even moreremove no-longer-needed Makefile hackeryBump stdpp.More permissive `gmap_fmap_mono`.Prove that `fmap` on `option` and `gmap` is monotone.Merge branch 'big_opM_union' into 'master'Add `big_opM_union` and `big_sepM_union`.fix Coq 8.9 deprecation warningsBump std++.Property about bigops and replicate.Add missing `Implicit Type` and fix an unbounded variable.Merge branch 'robbert/fork_postcondition' into 'master'Turn global fork postcondition into a predicate over return values.Get rid of `irisG'`.Consistently state equalities in pure lifting lemmas with "post-state" on the LHS.Add CHANGELOG entry.Document `state_interp` and `fork_post`.Remove non-fork versions of pure lifting lemmas.Fine-grained post-conditions for forked-off threads.