Skip to content
Snippets Groups Projects
Select Git revision
  • atomic
  • ci/3.1.0
  • ci/debug
  • ci/janno/debug-opam
  • ci/janno/vmcast
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/robbert/into_val_pures
  • ci/stability
  • ci/value_constructor
  • fast_string
  • fix-class-apply
  • fix-export
  • fix-from-assumption-exact
  • fix-local-inductive
  • instance-nobody-open-proof
  • iris-3.0
  • iris-3.1
  • janno/metacoq
  • jh/done_contradiction
  • 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.013Feb121110985432131Jan302927262523222120191817161413129865422Dec21161514118423Nov22201918171612119630Oct2928272316151431Aug16Jul24Jun2215115432131May302928272625161514131211723Apr141311109872131Mar3029282725change statement of inv-open lemmas such that they do not force the invariant, and the 'inner step', to appear right next to each otherprove that we can always own an empty fragment of authLaTeX: change \set macrosprove that 'deleting' in the exclusive CMRA is a local updatefix Makefile attributionwakestpre: swap wp_value and wp_value'heap_lang: rename lifting lemmas so that the final forms do not have a primeupred: move the primes in the always lemmas to the more specific versionsmake some arrows nicersimplify our build instructions to just "make"bind types to scopes as early as possible, to functions get their arguments set appropriatelydocs: we are going to have namespacesdome more doc for gsubstremove some now-unnecessary scope annotationsMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqsupport using setup.tex from another directoryFactor out boring properties of contractive.More general and Global version of auth_timeless.Import notations last, otherwise things are not pretty printed.Rename heap_lang/heap_lang_tactics.v -> heap_lang/tactics.vDocument gsubst function and move to separate file.Put Lit notations in global scope.Multi argument recs.Right associativity of some heap_lang constructs.The uPred connectives ■, □ and ▷ should be right associative.Change FindPred to get better folding/unfolding behavior.Block simpl for of_val to avoid too much unfolding.Remove superflous brackers.Use ;; for seq, ; conflicts with lists.Shorter names for common math notions.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqfix Pred test. also make it more complicated.switch the language over to integersSet level of ✓ to 20 (just like ■, ▷ and □).Make language notations stable under simpl.heap_lang: Separate derived notions and notations into different filesChange some names related to the global ghost CMRA aroundMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqIntroduce the notion of "Frame Shift Assertions", and use to prove the rules about inv and auth at once for pvs and wpRevert "prelude: add notation for > and >= for all kinds of numbers"