Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/ralf/frame-frac
  • 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
  • ci/robbert/merge_sbi
  • ci/robbert/naive_solver
  • 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
34 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.028Jun27262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765432129Feb282726252423Merge 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.Use type classes instead of option hack to remove Trues while framing.Generalize 7c4416b6 to remove head "value ;;" expressions after any wp_ tactic.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqadd some comments explaining design decisionsTactic iSimplifyEq that substitutes Leibniz equalities that are in the proof mode context.Let wp_store to a wp_seq if possible.heap_lang notations for Some/None.Remove wp_case, add wp_match.More hlist stuff.Replace some non-unicode arrows.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqInclude jh_simplified_ressources in the CI branchesCorrectness proof of imperative summing of a tree.Put quantifiers in pvs and wp definition in same order as wsat.More heterogeneous list stuff.Remove lviewshifts.v and turn them into notations.Seal off mapsto, invariants, and ghost ownership.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqMerge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqNotation for n-ary non-expansive functions.Improve allocation lemmas for gmap.Prove list_singleton_local_update.Better statement of posivitity of option.Fix implicit arguments of dec_agreeC.Rename auth.own into auth_own.Introduce iDestruct num tactic.Make iSplit work on goals of the shape ⊣⊢.Fix some Params instances.Make local updates relational.Remove superfluous parentheses.Make exclusive stuff more consistent.