Skip to content
Snippets Groups Projects
Select Git revision
  • atomic
  • ci/3.1.0
  • ci/debug
  • ci/disable-ltac-backtrace
  • ci/janno/debug-opam
  • ci/janno/let_bind_envs
  • ci/janno/reduction_no_check
  • ci/janno/vmcast
  • ci/joe/compact_ipm
  • ci/maximedenes/instance-nobody-open-proof
  • ci/prophecy
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/ralf/set_unfold_elements
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/set_unfold
  • ci/robbert/tc_opaque
  • ci/stability
  • ci/value_constructor
  • 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.028Oct27262524232019181210975429Sep282726252421201918171615141198628Aug262423222120181776428Jul14121027Jun13128625May1712927Apr261913121175431Mar302824232221201615141211109765124Feb23222120181716151413121110987632130Jan2928272625242322212017131211109876543128Dec2726232221201918171615141312119expand changelogbump std++Add note about iIntros/iAlways to CHANGELOG.Make more use of the `direction` enum in the proof mode tactics.Tweak the proof mode docs.Support `->` and `<-` for pure equalities in proof mode intro patterns.document iAlwayschangelog and commentsMerge branch 'naught' into 'master'Plain instances for the big ops.core: don't use the turnstile inside the logicPort the core to use the plainness modality and prove it is non-expansive.Proofmode support for introducing the plainness modality.Plainness and persistence of implications and wands.Simplify soundness of the base logic.Proof mode instances for eliminating plain basic updates.Proof mode instances for the plainness modality.Avoid exponential proof search due to Plain → Persistent instance.Derived rules of the plainness modality.Add the plainness modality to the model of the base logic.Removed a stray proof mode lemma.Put heap_lang's let/lambda/rec at level 200.Some updates to the CHANGELOG.list more renamingsexpand changelogdon't try to be smart about having an up-to-date opamstart on the changelog for 3.1Weaken the associativity axiom of the Dra class.Add saved predicatessavedpredsavedpredMerge branch 'big_rename' into 'master'Replace/remove some occurences of `persistently` into `persistent` where the property instead of the modality is used.Rename `always` → `persistently` (the persistent modality).Rename `PersistentP` → `Persistent` and `TimelessP` → `Timeless`.Rename `Persistent` → `CoreId` (camera elements whose core is itself).Consistently de-capitalize acronyms.Rename `Timeless` → `Discrete` (discrete OFE elements).Rename `Discrete` → `OFEDiscrete` (OFEs whose elements are all discrete).Missing `IntoForall` instance for later.Make `iIntros (?)` introduce ∀s/pures under ▷ and □ modalities.Make `iDestruct ... as (cpat) "..."` work on '⌜φ⌝ ∧ P` and `⌜φ⌝ ∗ P`.