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.010Sep331Aug30292413112131Jul24231713976543230Jun29282625232221201918171615141312111098654131May30292825242320181715141198743227Apr26252423222120191811109654331Mar28272422212019161514131298765432128Feb2726252423222120191816151413update CICoq 8.10 is broken for output as wellMerge branch 'ci/3.1.0' into 'iris-3.1'update a commentAddress Ralf's feedback in .gitlab-ci.yml.Port new CI to iris-3.1.we are compatible with Coq 8.8undo accidental editExport Ascii for compat with new Coqfix paradox pseudo-masksFix typo in the documentation. Thanks to Joe for pointing that out.Update lemma for frac_auth with fraction 1.CI issue was upstream in opam, partially revert the changesupdate CIupdate CIFix typo in comment.Clarify comment.Support `iInduction ... using`; this closes issue #204.Merge branch 'insert_alloc_local_update' into 'master'Added a new lemma to allocate fragmented ownership in unital gmaps while updating the full ownershipUpdate README.md even moreUpdate README.mdmore MoSeLbump std++; update test suite makefileclean betterMerge branch 'ci/ralf/atomic' into 'master'add iGPS to list of case studies we maintainchangelogthe rewrite problem now has an issue numberdefine a general make_laterable construct and use it for atomic updatesadd lemma to prove atomic WP without seeing a QSequential triples with a persistent precondition and no initial quantifier are atomicadd a tactic for the final introduction of an atomic accessorenable iMod to run an atomic updateadd a weak increment operation that knows it does not raceProve that atomic triples imply "normal" triplesAdd some lemmas about mapsto to the atomic_heap interface; use IntoVal for alloc specalso test Coq 8.8.1make atomic_heap a typeclass and add some notation for itUse telescopes for atomic accessors, updates and triples; improve mask handling; add notation for all of them
Loading