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.030May292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765432129Feb282726252423222120191817More consistent naming for CMRA/uPred duplication lemmas.More prelude/base rearrangement.Functions are inhabited.Use proper notations in saved_prop.COFE on gname.Add notation iPrePropG.Deallocation is a local update.CMRAs with partial cores.Get rid of non-expansiveness in uPred.Split monotonicity and closedness fields of uPred.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqIntroduce a canonical structure for CMRAs with a unit element.Generalize from_option and define default using it.Remove PropHolds type class.More inversion properties for equiv/dist on option.Sum COFE.Injectivity instances for prod/sum.Change notation of prod functor to look like a prod instead of a pair.Lift a relation to the sum type.Reorganize prelude/base: group stuff that belongs together.Define dist on option using option_Forall2.Some general option_Forall2 properties.Turn some -> arrows into →.add missing file: lviewshiftsProve another lemma to open invariants that we only know by namespace.Put option stuff in algebra/cmra and algebra/cofe.Tweak the algebraic hierarchy.Change notations of big_ops for upred.Make use of {[ x1; .. ; xn ]} set notation in barrier proof.Prove big_sepM_delete.Error message when =>[H1 .. Hn] is used and goal is not a pvs.Merge iAssert and iPvsAssert.Clean up some useless scope delimiters.Flip order of arguments of iAssert/iPvsAssert.Make specialization patterns for persistent premises more uniform.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqCMRA structure on lists.Make some names more consistent.Misc property about the product CMRA.