Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/robbert/big_op_binder
  • ci/robbert/contractive_ne
  • ci/robbert/coq_bug_7773
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/frame_fractional
  • ci/robbert/iFrame
  • ci/robbert/into_fupd
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/mapsto_persist
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • 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
36 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.02Jul130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765432129Feb2827262524Lifting 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.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqSome properties of imapEnable $-prefixes in ssr-like {H1 .. Hn} intro-patterns to perform framing.Simplify spec_patterns parser by using a mutual fixpoint.Bring back wp_bindiCreate eauto hint for iPvsIntro.Add wp_value_pvs' (like wp_value').Fix order of imports.Make all the wp stuff (lemmas and tactics) preserve view shifts.Split IsPure into IntoPure and FromPure.Some clean up.Oops!Move some proof mode classes to their own file.Define discreteUR constructor.Remove useless type class instance.Revert "Counting CMRA" because it is already in cmra.v (called natR).Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqRename type classes in proof mode.Move class for later stripping to proofmode.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqCounting CMRAImprove solve_proper a bit.Fix inconsistent name later_exist'.Make iSplit work with later and always.Rename uPred_const -> uPred_pure.