Skip to content
Snippets Groups Projects
Select Git revision
  • ci/3.1.0
  • ci/debug
  • ci/disable-ltac-backtrace
  • ci/for_proph
  • ci/janno/debug-opam
  • ci/janno/let_bind_envs
  • ci/janno/vmcast
  • ci/joe/compact_ipm
  • ci/joe/compact_ipm_remaining
  • ci/joe/compact_ipm_simple
  • ci/maximedenes/instance-nobody-open-proof
  • ci/mtac2-tt
  • ci/prophecy
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/ralf/set_unfold_elements
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/into_val_pures
  • 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.026Oct2524232019181210975429Sep282726252421201918171615141198628Aug2624232221201776428Jul14121027Jun13128625May1712927Apr261913121175431Mar302824232221201615141211109765124Feb23222120181716151413121110987632130Jan2928272625242322212017131211109876543128Dec2726232221201918171615141312119876Weaken the associativity axiom of the Dra class.Merge 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.Proof mode instances for the plain modality.Avoid exponential proof search due to Plain → Persistent instance.Derived rules of the plain modality.Add the plain modality to the model of the base logic.extractor: support grabbing logs from local all-artifacts zip folderfix gitlab-extractupdate READMEand another test that depends on the barrierremove a test that depends on the barriermove barrier to new iris-examples repo; test that repo after each Iris commitCI: rename REV parameter to IRIS_REV for iris.dev buildsCI: syncCI: rename jobs for consistencyreverse-deps trigger: set Iris revisiontrigger an iris-atomic build in the deploy stagefix typo in .gitlab-ci.ymlrename 2nd stageupdate CI system