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.011Jul65432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765432129Feb28272625Strengthen some gmap lemmas by using Leibniz equality.LeibnizEquiv instance for unit.Remove CollectionOps class.ProofMode.md: typoslib/spawn: make proofs more readable / steppableMerge branch 'jh_state_lifting'More proof mode docs.And another one.Fix typo.Fix some spaces/tabs/0 width spaces in the proof mode docs.Frame under a wand.Rename fallthrough (instances) into default.Write some proof mode documentation.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq Get rid of phi predicates everywhereFix instance for ndisjoint.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqfix a weird typoCorrectness of monotone counter.Persistence of auth_own.Give the left instance of FromAnd (P1 ★ P2) P1 P2 precedence.Notation for max and min.Mononicity of auth_own.CMRA on nat with max as op.Qp is inhabited.Lifting lemmas : get rid of \phi when it has became uselessLifting lemmas : make the initial state appear under an existential under the view shift. This is still sound, but slightly more expressive.Add lemma pure_iff.Ensure that solve_ndisj "solves", it either succeeds or fails.Use ndot_ne_disjoint more eager so it expands definitions.Local update for natLocal updates for sumsMerge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqMake Program obligations Transparent by default.New lemma : cmra_update_valid0. This let us prove a FP update using the additionnal hypothesis that the source is valid at step 0.New lemma aboud maps : fmap_deleteClean up some ndisjoint stuff in the proofmode tactics.Tweak tests/one_shot.Improve ndisj hint database.Hack to avoid getting String.length instead of List.length.