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.030Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765432129Feb2827262524Oops!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.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.