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.012Feb1110985432131Jan302927262523222120191817161413129865422Dec21161514118423Nov22201918171612119630Oct2928272316151431Aug16Jul24Jun2215115432131May302928272625161514131211723Apr141311109872131Mar302928272524simplify 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"use < and <= instead of > and >=Missing cmra_preserving lemmas.change auth_pvs to have a more genrally useful formMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqtweak heap_lang sugarMore AlwaysStable stuff.prelude: add notation for > and >= for all kinds of numbersmake solve_ne slightly more robustauth.v: do not depend on argument order of commutative