Skip to content
Snippets Groups Projects
Select Git revision
  • atomic
  • ci/janno/vmcast
  • ci/mtac2-tt
  • ci/ralf/atomic
  • ci/ralf/pm_red
  • ci/ralf/telescopes
  • ci/robbert/overloaded_wp
  • fast_string
  • gen_proofmode
  • iris-3.0
  • iris-3.1
  • janno/fix-566
  • janno/iframe-cbv
  • janno/iframe-no-upd
  • janno/ipm-strings
  • janno/ipm-strings-upstream
  • janno/metacoq
  • janno/try-HB
  • jh/done_contradiction
  • jh/evar_iframe
  • 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
30 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.016Jun1514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765432129Feb28272625242322Fix some Params instances.Failed attempt at improving performances of pairs by using inductivesjh_inductive_pa…jh_inductive_pairsMake 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.Simplify the definition of Exclusive. Use it for gmap.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq