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.017Jun161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765432129Feb28272625242322Rename 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.Rename box_slice into slice.Change the Coq scope notations for viewshifts into parsing only.Notations for X ⊆ Y ⊆ Z.Generalize big_sepM_fn_insert and big_sepS_fn_insert.Make iFresh faster on environments containing evars.Tactic iFrame (without args) that tries to frame all spatial hyps.Auto hints for the proof mode.