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.030Oct292827262524232019181210975429Sep282726252421201918171615141198628Aug262423222120181776428Jul14121027Jun13128625May1712927Apr261913121175431Mar302824232221201615141211109765124Feb23222120181716151413121110987632130Jan2928272625242322212017131211109876543128Dec27262322212019Use the sink modality in the proof mode.Proof mode class instances for the sink modality.The sink modality.A rather ad-hoc IntoSep rule for `■ ▷ (P ∗ Q)`.Fix error message of iDestruct.Use cheaper iDestructHyp in iInv.Allow stripping of timeless ▷s below ■ modalities.Generalize iAlways to also introduce ■ modalities.Strip laters below ■ and □.More consistent naming, e.g. bare_later -> later_bare_2.Also add Affine instances for empty/nil big ops.Added Affine instances for big ops.Swap names of bare_and_l and bare_and_r.Some proofmode tweaks for the bare modality.The bare modality is also persistent.Make iEmpIntro succeed in a non-empty, but affine, spatial context.Explicitly unfold some definitions.Drop positivity axiom of the BI canonical structure.Define `Persistent P` as `P ⊢ □ P` instead of `□ P ⊣⊢ P`.Port counter examples to arbitrary affine BIs.Change the order of some IntoWand premises to avoid backtracking.Make iAssumption work when the whole remaining spatial context is affine.Remove axiom that emp is timeless.Iterated conjunction for lists.Simplify box axioms.Generalize proofmode.Remove useless cast.Merge branch 'fupd_plain' into 'master'Rules for fancy updates and plain propositions.add disjointness change to changelogMerge branch 'ralf/atomic' into 'master'expand commentsadd a strong form of atomicity, for weak forms of weakest-prerevert accidentally changed changelogImplement `iRewrite` using type classes.State `internal_eq_rewrite` in the logic.Merge branch 'jh/bottom_notation' into 'master'Notation for disjointness: replace ⊥ with ##, so that ⊥ can be used for bottom.opam CI: more verbose output; more robust opamopam-ci: silence accidental output