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.026Oct252422212019181312111075432130Sep27262019181210331Aug3029241713112131Jul242319181713976543230Jun2928262523222120191817161514131211109876543131May302928272524232018171514111098743230Apr2928272625242322212019181211109654331Mar3028272422212019Prepare 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.9get rid of observations in ownP, they just make porting harderRemove spurious import.Replace more occurences of /\ by unicode ∧.Add type annotation.Use unicide ∧ and ∃.Add missing type in a signature.Bump 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 nits