Skip to content
Snippets Groups Projects
Select Git revision
  • arrays
  • atomic
  • atomic_resolve_alternative
  • cas_resolve
  • ci/3.1.0
  • ci/debug
  • ci/disable-ltac-backtrace
  • ci/janno/debug-opam
  • ci/janno/vmcast
  • ci/joe/compact_ipm
  • ci/maximedenes/instance-nobody-open-proof
  • ci/prophecy
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/tc_opaque
  • ci/stability
  • ci/value_constructor
  • fast_string
  • 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.013Feb121110985432131Jan302927262523222120191817161413129865422Dec21161514118423Nov22201918171612119630Oct2928272316151431Aug16Jul24Jun2215115432131May302928272625161514131211723Apr141311109872131Mar3029Internalize specs of valid and equiv for all cofe/cmras.Internalize specs of valid and equiv for all cofe/cmras.add a derived 'skip' to heap_langrename the logic's hint DBcreate a hint database for solving some simple uPred'sUse new Import/Export syntax everywhere.Remove FIXME.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqtry out a new Coq 8.5 syntax to shorten long Import linesMake reflexivity hints work for evars.try to rely more on eauto - and fail and leave some FIXMEschange 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.