Skip to content
Snippets Groups Projects
Select Git revision
  • ascii-sections
  • basic-dune
  • bi_pure_scopes
  • doc-equalities
  • explicit-vdash
  • fix-497-hint-immediate
  • fix-notation
  • fupd-commutes
  • inv_exc_0_ipm
  • later-credits-drop
  • later_impl_experiments
  • later_impl_test
  • master default
  • more-convenient-fupd_proper
  • no-bi-canonical
  • notations
  • paolo/tc-strict-resolution-backport
  • periscopes
  • periscopes-v2
  • seal_ires
  • iris-4.3.0
  • iris-4.2.0
  • iris-4.1.0
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • iris-3.2.0
  • 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
39 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.02Nov31Oct302928272625242019181210975429Sep282726252421201918171598628Aug26242322201776428Jul14121027Jun13128625May1712927Apr261913121175431Mar30282423222120161514121110976124Feb2322212018171615141312111097632130Jan2928272625242322212017131211109876543128Dec27262322212019181615141312119Remove notations for bi_bare and bi_persistently.Typo : sbi_mixin_internal_eq_ne->bi_mixin_internal_eq_neset up CI and automatic opam publication for gen_proofmode. do NOT merge into master!update build systemMake algebra/proofmode_classes.v no longer depend on base_logic.Port fixpoints to BIs.Allow to move non-affine stuff to the persistent/pure context if the goal is absorbing.Missing timeless instances.Use 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 comments
Loading