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.028Mar2423222120161514121110976124Feb2322212018171615141312111097632130Jan2928272625242322212017131211109876543128Dec2726232221201918161514131211987652130Nov2928272625242322212019181716151098765432131Oct3028272625222118Consider simpl and clearing introduction patterns as persistent.Version of iPoseProof with intro pattern.Enable solve_ndisj to handle unions on the LHS.Merge branch 'gen_big_op' into 'master' Add an example why we need WeakMonoidHomomorphism.Make big_opL type class opaque.Derive monoid_right_id.Use generic big op lemmas instead of uPred specific ones when possible.Generic big operators that are no longer tied to CMRAs.Remove Hints and Instances that are no longer needed.Redefine big ops to get more definitional equalities.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqRefactor the resources for ticket lockBetter error message when the hypothesis given to iDestruct does not exist.make solve_to_val work when there are still locks in the goalProve missing proper instances for inv`FromAnd true` instances for big ops and ownership.Merge FromSep and FromAnd classes.No longer allow ownership of persistent elements to be split.Fix some typos in comments.work around Coq bug 5401 breaking 'Print HintDb typeclass_instances'Remove duplicate lemmas for agree.Some missing unicode arrows.Some simple lemmas for fractional.update std++Show an interesting lemma about the coreLet iAlways clear spatial context.Fix issue #80: better error message when hyps are missing.Remove old debugging code.Misc proof mode clean up.New internal IPM tactic: env_reflexivity.Remove Hint Mode that was already declared elsewhere (in classes.v).Support nat tokens in the tokenizer.Merge branch 'docs' into 'master' IntoModal --> FromModal in the docsUpdated the notation for lifting in ProofMode docsEnable solve_ndisj to solve `∅ ⊆ X`.Small tweaks.Fix possible divergence in framing.Better support for framing persistent hypotheses.