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
  • iris-3.0
  • iris-3.1
  • janno/metacoq
  • jh/done_contradiction
  • jh/evar_iframe
  • jh/independent_metric
  • jh/sprop_upred
  • jh_inductive_pairs
  • joe/bupd_derived
  • 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.03Nov2131Oct302827262522211817161514131210976543228Sep272120191514131298765432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130JunForgot something as part of 7d74f654.Merge branch 'new_star' into 'master' Use symbol ∗ for separating conjunction.Merge branch 'ralf/texan' into 'master' New notation for Texan triple postconditions: Use 'RET' as keyword to indicate the return valuecurried Texan triplesChange the way we handle view shifts in post-conditionsuse texan triples for some more subtle casesInstantiate foralls behind boxes by removing those.Remove tests/atomic.v; the atomic stuff is all in iris-atomicAdd notation l ↦{q} -.tests/counter.v: explain purposeupdate iris.stygive dedicated names to the type of ghost names, invariant namesCHANGELOG: mention the moving-things-aroundLemmas for updates that take a step.Merge branch 'robbert/invariant'Move program_logic stuff that does not depend on the language to base_logic/lib.Remove dependency of fancy updates on the program language.Merge branch 'move-global-func' into 'master' Add flipped mono instances for wand, impl, forall, exist.Turn short-circuit && and || into definitions.Also create a wand when reverting a persistent hypothesis.ElimModal instance for □.Move global functor to base_logicFix typo.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqMakefile: hide recursive make callsAllow framing in negated specialization pattern.Fix inefficiency in proof mode.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqfix compilation with Coq 8.6 (for some reason, that 'apply:' diverges)fix README linkstactics: rename auto_proper => auto_equivimprove f_equiv docMerge branch 'janno/hoare-notation' into 'master' add texan triples in uPred_scoperepeat notation annotations for quantifiers, just to be sureSimplify Texan triple notations.add a later in texan triples