Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.03Nov231Oct302928272625242019181210975429Sep282726252421201918171598628Aug26242322201776428Jul14121027Jun13128625May1712927Apr261913121175431Mar30282423222120161514121110976124Feb2322212018171615141312111097632130Jan2928272625242322212017131211109876543128Dec27262322212019181615141312Merge commit '17b8' into gen_proofmodeMerge commit '38b6' into gen_proofmodeMerge commit '92c7' into gen_proofmodeSimplify uses of AffineEnv by making it easy to prove when the BI is affine.Fix wrong naming convention for IntoExcept0 instances.Merge commit 'f5a5f' into gen_proofmodetry to work around yet another opam silliness`IntoForall` and `FromForall` instances for `except_0`.Simplify proof of `forall_timeless`.Prove `except_0_forall` in both directions.Merge branch 'proofmode_notation_fix' into 'master'Hide the proof mode entailment behind a definition.Renaming: sink->absorbingly bare->affinely.Move special purpose class `AsRec` to the only place it is used.Add an `AsVal` type class.Remove some wp lemmas that are not used for implementing tactics anymore.Remove some unused eauto arguments.Remove 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.