Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/robbert/big_op_binder
  • ci/robbert/contractive_ne
  • ci/robbert/coq_bug_7773
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/frame_fractional
  • ci/robbert/iFrame
  • ci/robbert/into_fupd
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/mapsto_persist
  • 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
36 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.013Apr121175431Mar302824232221201615141211109765124Feb2322212018171615141312111097632130Jan2928272625242322212017131211109876543128Dec2726232221201918161514131211987652130Nov2928272625242322212019181716151098765432131Oct3028272625Also 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.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.