Skip to content
Snippets Groups Projects
Select Git revision
  • ascii-sections
  • basic-dune
  • bi_pure_scopes
  • doc-equalities
  • explicit-vdash
  • fix-497-hint-immediate
  • fix-notation
  • fupd-commutes
  • inv_exc_0_ipm
  • later-credits-drop
  • later_impl_experiments
  • later_impl_test
  • master default
  • more-convenient-fupd_proper
  • no-bi-canonical
  • notations
  • paolo/tc-strict-resolution-backport
  • periscopes
  • periscopes-v2
  • seal_ires
  • iris-4.3.0
  • iris-4.2.0
  • iris-4.1.0
  • 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
39 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.023Jun2120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765432129Feb282726252423Tactic 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.Move update stuff to its own file (it used to be in cmra.v).More consistent names for (local) updates.Make additional carrier fields in structures anonymous.Use projections in the instance of Timeless for pairsPut the carrier also in the back of canonical structures.Make iDestructing of existentials go through always.Define projections of cofeT, cmraT and ucmraT as Hint Extern.Some canonical structure instances for heap_lang.Strenghen pair_op.Setoid instances for fmap on fin_map and option.Fix type in lock.CMRA on nat.Small clean up.