Skip to content
Snippets Groups Projects
Select Git revision
  • atomic
  • ci/3.1.0
  • ci/debug
  • ci/janno/debug-opam
  • ci/janno/vmcast
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/robbert/into_val_pures
  • ci/stability
  • ci/value_constructor
  • fast_string
  • iris-3.0
  • iris-3.1
  • janno/metacoq
  • jh/done_contradiction
  • jh/evar_iframe
  • jh/independent_metric
  • jh/sprop_upred
  • jh_inductive_pairs
  • joe/bupd_derived
  • 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
30 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.024Aug1713112131Jul242319181713976543230Jun2928262523222120191817161514131211109876543131May302928272524232018171514111098743230Apr2928272625242322212019181211109654331Mar30282724222120191716151413121198765432128Feb27262524Export Ascii for compat with new CoqShow that bupd can be (essentially) defined in terms of other connectives.joe/bupd_derivedjoe/bupd_derivedfix paradox pseudo-masksFix typo in the documentation. Thanks to Joe for pointing that out.Update lemma for frac_auth with fraction 1.kids, never forget to pull before introducing changes (I am the kid, no offence meant to nobody)bumped Mtac2's commitadapting to last change in Mtac2/masterBack to Mtac2/master.Use Mtac2/janno/cps_unify.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 makefileBump Mtac2 commit.Revert "Make heap_lang/proofmode.v universe polymorphic."Make heap_lang/proofmode.v universe polymorphic.Revert "Make heap_lang/tactics.v universe polymorphic."Make heap_lang/tactics.v universe polymorphic.Make proofmode/tactics.v polymorphic.clean 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" triples