Skip to content
Snippets Groups Projects
Select Git revision
  • atomic
  • ci/3.1.0
  • ci/debug
  • ci/janno/debug-opam
  • ci/janno/vmcast
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/robbert/into_val_pures
  • ci/stability
  • ci/value_constructor
  • fast_string
  • iris-3.0
  • iris-3.1
  • janno/metacoq
  • jh/done_contradiction
  • jh/evar_iframe
  • jh/independent_metric
  • jh/sprop_upred
  • jh_inductive_pairs
  • joe/bupd_derived
  • 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
30 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.020Oct19181312111075432130Sep27262019181210331Aug3029241713112131Jul242319181713976543230Jun2928262523222120191817161514131211109876543131May302928272524232018171514111098743230Apr2928272625242322212019181211109654331Mar3028272422212019171615141312Bump Mtac2-8.8 commit.fix compatibility with Coq 8.7Merge branch 'ralf/prophecy' into 'master'Allow `IntoVal` to take pure steps.ci/robbert/into…ci/robbert/into_val_puresWeaken `PureExec φ n e1 e2` so that it can take `>= n` steps.Move `Atomic`, `IntoVal` and `AsVal` instances to lifting.Automate proofs of `Atomic` instances.Misc white space nits.Curry parA specific constructor for injecting values in expressionsnote some FIXMEsmore nitsuse 'proph' instead of a notation, and rename type of prophecy variables to proph_idmore nitsgeneralize to lists of observations per program stepfix nitsuse record for heap_lang stateMerge remote-tracking branch 'origin/master' into ralf/prophecy`(P → Q) ⊣⊢ ∃ R, R ∧ <pers> (P ∧ R -∗ Q)` holds for general BIs.Bump Mtac2-8.8 commit.Bump Mtac2-8.8 commit.Bump Mtac2-8.8 commit.fix typoSwitch to iris-ci/debug.ci/janno/debug-…ci/janno/debug-opamMerge branch 'ci/ralf/ci' into 'mtac2-tt'Switch to Ralf's opam2 branch of iris-ci.Bump Mtac2-8.7 commit.test and support Coq 8.8.2Merge branch 'robbert/pure_exec_nsteps' into 'master'Add changelog entry for `PureExec`.Support multiple steps in `PureExec`.Make use of `[#]` in `solve_…` heap_lang/tactics.Bump Mtac2-8.8 commit.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqUse only printing on notations for lambdas.heap_lang consistent spellingchangelogwhitespace tweaksdocument some heap_lang design choicestweak WP def.n and fix eauto in heap_lang