Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.017Jun161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765432129Feb282726252423Merge 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.hack makefile to fix coqchk invocationbenchmark visualize: but legend next to graphTurn some "case _ :" occurences into "case:'.Name some intro-ed stuff.Not all [Qp]s are [frac]s, so make the notation only parsing.Simplify prod_leibniz.useless ArgumentsMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqSimplify frac : use a pair of a rational and a carrierMake iAssert infer the cmra M of the asserted uPred M.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqGot rid of one_shotUse |==> syntax for 'preserve pvs' specialization pattern.