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
  • fix-class-apply
  • fix-export
  • fix-from-assumption-exact
  • fix-local-inductive
  • instance-nobody-open-proof
  • iris-3.0
  • iris-3.1
  • janno/metacoq
  • jh/done_contradiction
  • 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.05Sep432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr2726252421201918Viewshifts that take a step.Rename envs_persistent → env_spatial_is_nil.Tweak.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqMore lemmas about Some and included.Double negation elimination for pure props holds under nnvs modality.Relate ≼ and ⊆ on coPset and gset.Prove variants of CMRA facts for CMRAs with = ↔ ≡.Relate ≼ to is_Some and dom.Introduce notation excl' (like Excl' and ExclNone').Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqGroup iff properties in uPred.Prove that uPred_pure commutes with the first-order connectives.Reorganize double negation equivalence proof; direct proof of transitivityProve more rules for always in the logic.Prove more later properties in the logic.Prove Timelessness of pure in the logic.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqProve Timeless instances in the logic instead of the model.Remove ownM_something.Prove later_intro in the logic; it follows from Löb.Make cmra_timeless_included_r consistent with cmra_timeless_included_l.Prove timelessness of exist in the logic.Fixes for compilation with Coq 8.6.Make namespace type classes opaque.Improve error message of iInv when mask condition cannot be solved.Make gmap_empty Opaque to avoid simpl unfolding it.Turn iProp into a notation.Some ectx_language properties.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqTurn out Coq 8.5 already comes with a module to get lia without axioms: Liarvs is (classically) equivalent to a kind of double negationUse the big op over lists in the definition of weakestpre.More big op properties.Add weakest-pre version atomic_tripleSome clean up/tweaks of locks.More simpl to reduce %V scopes.Merge branch 'lock-iface' into 'master' Abstract lock interfaceUse simpl more to get rid of %V scopes following 6d038c53.