Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
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
Created with Raphaël 2.2.019Apr13121175431Mar302824232221201615141211109765124Feb23222120181716151413121110987632130Jan2928272625242322212017131211109876543128Dec272623222120191817161514131211987652130Nov2928272625242322212019181716151098765432131Oct302827styleShorten the agreement proofs and bring the construction closer to the one in the paper.Lemma timeless_iff_0.Reverse direction of wp_bind.Reorganize proofmode tests.Also keep track of whether a hypothesis is persistent in IntoWand.Fix error message of iApply.document JH's recent change in the CHANGELOGMerge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqadd Aleš's proof that agree is not completeMerge branch 'jh/cmr_morphisms' into 'master' proofmode tests: use a sectionclose cancellable invariants under logical biimplicationcancellable invariants are contractiveLet iSpecialize with a hypotheses behave like iAssumption.provide functor for cancellable invariantsA notion of CMRA morphims based on the compatibility with validity, core and composition.Typos.Upred : explain why things are how they are.Upred is isomorphic to some kind of monotonous SProp predicate. (WIP)jh/sprop_upredjh/sprop_upreddocs: fix some typosdocs: formatting fixesAdd visible notation for empty context in proofmodeConsider 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.