Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
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
Created with Raphaël 2.2.027Jul2625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765Declare inG arguments of own_* implicit but not maximally inserted.Iterated later modality.Revert "Make the types of the finite map type classes more specific."Make the types of the finite map type classes more specific.don't backtrace on the operatorMerge remote-tracking branch 'MPI-SWS/master'Use auth_update_no_frame in boxes.More consistent names for gset updates.FP update for auth without frame.Relate subseteq on collections to the extension order.Make type class inference for inG less eager.Revert "Hack to delay type class inference in iPoseProof."Hack to delay type class inference in iPoseProof.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqFixed some typos in the appendix.Rename some proofmode stuff to be no longer primitive view shift specific.Proofmode type class instances for raw view shifts.docs: update CMRA constructions for partial coredocs: update (CM)RA algebra axioms to aprtial coresupdate CHANGELOGrename: preserving for a partial order -> monotoneupdates iris.styadd a CHANGELOGNew notion of raw view shifts.Simplify TimelessElim class.Fix implicit arguments of gset CMRA.Generalize iTimeless tactic.Move tac_exist from classes to coq_tactics where it belongs.More documentation of [coPset].Remove forgotten admit in f2c246c6.Remove unused and not really maintained Hoare lifiting lemmas.Move local updates to separate file.Simplify weakestpre_fix construction.Cofe on the function space A → B where A : Type and B : cofeT.Rename cofeMor → cofe_mor and cofe_mor → cofe_morC for consistency.Make level of -n> the same as →.Forgot to commit prelude/sorting, this fixes 6dbe0c27.CMRA structure on coPset.Local update on gset.CMRA structure on gsets that avoids the indirection via maps.