Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • adjust-focused-goal
  • atomic
  • avoid-deprecated-arith
  • byte-strings
  • bytes-ident
  • 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
  • cmra-iso
  • cmra-restrict-valid
  • coqide-unicode-config
  • dfrac-smart-constructor
  • dfrac-valid-arg
  • document-ipm-classes
  • 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
Created with Raphaël 2.2.025Oct24232019181210975429Sep282726252421201918171615141198628Aug262423222120181776428Jul14121027Jun13128625May1712927Apr261913121175431Mar302824232221201615141211109765124Feb23222120181716151413121110987632130Jan2928272625242322212017131211109876543128Dec2726232221201918171615141312119876Rename `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 systemopam: don't use the shell for no good reasonBump coq-stdpp.Coq CI does not need opam.pins any moreMerge branch 'ilocked' into 'master'Proof mode instances for [tc_opaque].Merge branch 'ci/primproj' into 'master'use sections to scope options