Skip to content
Snippets Groups Projects
Select Git revision
  • ci/3.1.0
  • ci/debug
  • ci/disable-ltac-backtrace
  • ci/for_proph
  • ci/janno/debug-opam
  • ci/janno/let_bind_envs
  • ci/janno/vmcast
  • ci/joe/compact_ipm
  • ci/joe/compact_ipm_remaining
  • ci/joe/compact_ipm_simple
  • ci/maximedenes/instance-nobody-open-proof
  • ci/msammler/iris-coq-seal_big_opM
  • ci/mtac2-tt
  • ci/prophecy
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/ralf/set_unfold_elements
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • 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
31 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.024Mar232221201615141211109765124Feb23222120181716151413121110987632130Jan2928272625242322212017131211109876543128Dec272623222120191817161514131211987652130Nov2928272625242322212019181716151098765432131Oct302827262522Merge 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'WIP: try to prove more rules for salwaysralf/salwaysralf/salwaysderived strong always modality; needs some new primitive lawsRemove 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.make fractional lemmas use AsFractional