Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/ralf/frame-frac
  • 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
  • ci/robbert/merge_sbi
  • ci/robbert/naive_solver
  • 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
34 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.030Aug2928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr27262524212019181514131211109Prove timelessness of exist in the logic.Fixes for compilation with Coq 8.6.Make namespace type classes opaque.Improve error message of iInv when mask condition cannot be solved.Make gmap_empty Opaque to avoid simpl unfolding it.Turn iProp into a notation.Some ectx_language properties.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqTurn out Coq 8.5 already comes with a module to get lia without axioms: Liarvs is (classically) equivalent to a kind of double negationUse the big op over lists in the definition of weakestpre.More big op properties.Add weakest-pre version atomic_tripleSome clean up/tweaks of locks.More simpl to reduce %V scopes.Merge branch 'lock-iface' into 'master' Abstract lock interfaceUse simpl more to get rid of %V scopes following 6d038c53.get rid of a fixed TODOUse simpl to get rid of some %V scopes delimiters go away.Also use %E scopes in notations for Hoare triples.Merge remote-tracking branch 'mpi/janno/early-scopes'Define E and V scopes in program_logicMake iIntoEntails work when the entails is hidden under a delta.Fix typo that I forgot to git commit --amend.Rename uPred_now_True → uPred_except_last.Prove later_exist_1 in the logic.Cancelable invariants.Make thread_local a bit more consistent.Big ops over lists as binder.Make big ops opaque for type classes.More timeless and persistent instances for big ops.Remove obsolete comment.docs: fix a quantifiersdocs: fix \box propertiesdocs: fix V being about any CMRA; fix V's timeless axiomSimplify incr_2_safe.Provide a user-side example of atomic_tripleFix FIXME in atomic.vMerge branch 'atomic' into 'master'
Loading