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.031Oct2927262524222119181311754330Sep2618121031Aug2413112131Jul24231713976543230Jun29282625232221201918171615141312111098654131May30292825242320181715141198743227Apr26252423222120191811109654331Mar28272422212019161514131298765432128Feb27262524232221Merge branch 'robbert/fupd_new_axioms' into 'master'Get rid of useless IntoVal uses.New lemma `step_fupdN_wand`, and use instead of `step_fupdN_mono`.Adapt adequacy of total weakest preconditions to use adequacy of fupd.Allow introduction of `∀` under `|={E1,E2}=>` in case the predicate is plain.Document new fupd+plainly laws.Comment about BiFUpdPlainly and affine BIs.A more principled set of axioms for fupd+plainly.Merge branch 'value_constructor' into 'master'Add comment; fix test tests/heap_lang.v.Changelog.wp_pures.Move `Atomic`, `IntoVal` and `AsVal` instances to lifting.Automate proofs of `Atomic` instances.A specific constructor for injecting values in expressionsSome missing parameters.Some useful BI derived lemmas.Remove spurious type annotations (there is a `Implicit Type` here).Close issue #218.For the timing jobs, build our own ocamlProve `E2 ⊆ E1 → P ={E1,E2}=∗ P`.Notation `P ={E1,E2}▷=∗^n Q`.A comment explaining the `invG` submodule.Prove `(|==> ∀ x, Φ x) ⊣⊢ (∀ x, |==> Φ x)` for plain `Φ`.Use new `|={E,E'}▷=>^n` notation at more places.Tweak a proof.Proper pretty printing of new `|={E,E'}▷=>^n` notation.Merge branch 'joe/fupd_adequacy' into 'master'Use explicit names in some scripts, re-organize fupd plainly derived laws, adjust wsat import/export.Use plainly modality instead of typeclass in BiFUpdPlainly interface.Modify adequacy proof to not break the 'fancy update' abstraction. Modify fupd plainly interface and add new derived results.Coq 8.9 is no longer brokenstart testing with Coq 8.9get rid of observations in ownP, they just make porting harderRemove spurious import.Replace more occurences of /\ by unicode ∧.Add type annotation.Use unicide ∧ and ∃.Add missing type in a signature.fix compatibility with Coq 8.7