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
  • fix-class-apply
  • fix-export
  • fix-from-assumption-exact
  • fix-local-inductive
  • instance-nobody-open-proof
  • iris-3.0
  • iris-3.1
  • janno/metacoq
  • jh/done_contradiction
  • 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.013Jun1211109765432131May302928272625242321201916151312987642130Apr29272625242317168729Mar26222019171615141376543128Feb27262524232221201816137653130Jan2928272625242322191817161514131110225Dec22212019181514131210876330Nov292827262220161211986131Oct292726252422212019181312111075432130Sep27262019181210331Aug3029241713112131Jul242319181713docs: remove some commented-out outdated rulesMerge branch 'ralf/adequacy' into 'master'avoid some evarstweak adequacy: treat stuckness like the other WP indices`IntoSep` instance for `tc_opaque`.Coqdoc tweaks.Add lemma `meta_token_difference`.Merge branch 'robbert/adequacy' into 'master'move comments out-of-line to please the extremely picky macOS shelltry to fix test suite for macOSnote on macOS sed usagestate adequacy helper lemma more positivelyupdate docs for new adequacy statementRemove useless import.Tweak the proof of `wp_adequacy`.CHANGELOG entry.Comment about traces.A strong adequacy statement to rule them all.add sed script for frac_auth changeswith reftest normalization, whitelisting Coq 8.11 should not be needed any moreMerge branch 'ralf/frac_auth' into 'master'change frac_auth notationFix compilation with Coq master.Merge branch 'robbert/ufrac' into 'master'more failing unification placesnote a few places where we had to use ssreflect to force the use unification algorithmshow that owning a prophecy is exclusiveadd a lemma to easily combine two arbitrary mapsto (with different values)Add CHANGELOG.The unbounded fractional authoritative camera.Add notation for pointer arithmetic to heap_lang.fix build with Coq 8.10 and newersilence ambiguous paths warningsMerge branch 'robbert/locations_meta' into 'master'CHANGELOG entry.Comments for namespace_map.Comments for gen_heap.Use namespace map RA in meta.Namespace map RA.Attach ghost data to locations.