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.026Oct2524232019181210975429Sep282726252421201918171615141198628Aug262423222120181776428Jul14121027Jun13128625May1712927Apr261913121175431Mar302824232221201615141211109765124Feb23222120181716151413121110987632130Jan2928272625242322212017131211109876543128Dec2726232221201918171615141312119core: 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`.Use more informative tags `Strong` and `Weak` for the modalities.unified_persist…unified_persistent_modalityUnify plain and persistent modality.core: don't use the turnstile inside the logicupdate CONTRIBUTINGStart work on a benchmark data exporterPort the core to use the plain modality and prove it is non-expansive.Proofmode support for introducing the plain modality.Plainness and persistence of implications and wands.Simplify soundness of the base logic.Proof mode instances for eliminating plain basic updates.