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.029Oct2726252422212019181312111075432130Sep27262019181210331Aug3029241713112131Jul242319181713976543230Jun2928262523222120191817161514131211109876543131May302928272524232018171514111098743230Apr2928272625242322212019181211109654331Mar302827242221Automate proofs of `Atomic` instances.A specific constructor for injecting values in expressionsShow that bupd entails plausibly.robbert/plausiblyrobbert/plausiblyThe plausibly modality.Remove basic updates from the Iris model, and define them using plainly.robbert/bupd_be…robbert/bupd_be_goneSome missing parameters.Some useful BI derived lemmas.Bump Coq 8.8.1 to 8.8.2 in CI.Bump Mtac2-8.8 commit.Revert "Disable 8.7 CI job."Bump Mtac2-8.7 commit.Remove spurious type annotations (there is a `Implicit Type` here).Close issue #218.Disable 8.7 CI job.Fix error resulting from goal_dep merge.Bump Mtac2-8.7 commit.Bump Mtac2-8.8 commit.Do not always call vm_compute for `change_dep`.Prepare code for change to dep. goal type.Bump Mtac2-8.8 commit.For the timing jobs, build our own ocamlProve `E2 ⊆ E1 → P ={E1,E2}=∗ P`.Notation `P ={E1,E2}▷=∗^n Q`.Bump Mtac2-8.8 commit.Bump Mtac2-8.8 commit.A comment explaining the `invG` submodule.Prove `(|==> ∀ x, Φ x) ⊣⊢ (∀ x, |==> Φ x)` for plain `Φ`.Show that step fupd commutes with forall for plain predicates in Iris.joe/fupd_extrajoe/fupd_extraUse new `|={E,E'}▷=>^n` notation at more places.Tweak a proof.Proper pretty printing of new `|={E,E'}▷=>^n` notation.Merge branch 'joe/fupd_adequacy' into 'master'Use explicit names in some scripts, re-organize fupd plainly derived laws, adjust wsat import/export.Use plainly modality instead of typeclass in BiFUpdPlainly interface.Modify adequacy proof to not break the 'fancy update' abstraction. Modify fupd plainly interface and add new derived results.Coq 8.9 is no longer brokenMove `Atomic`, `IntoVal` and `AsVal` instances to lifting.ci/value_constr…ci/value_constructorAutomate proofs of `Atomic` instances.A specific constructor for injecting values in expressionsstart testing with Coq 8.9