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.07Jan5424Dec231918161110976432130Nov27262319181312111096543231Oct302927222120151413121098765432130Sep29282726242322211615141211108753230Aug29282412724Jul22211816151410432130Jun2926191817161513121187643130May29282726252423ensure that all Instance/Argument/Hint are qualifiedUse new class `IntoFUpd` in tactic `wp_value_head`.ci/robbert/into…ci/robbert/into_fupdAdd type class `IntoFUpd`.also add Local/Global to ArgumentsQualify all instances with Local or GlobalUse `Implicit Types` in HeapLang tests; this fixes compilation with Coq 8.11.Merge branch 'robbert/iMod_iInv_atomic' into 'master'Use `_` intro pattern for `True`.Apply 2 suggestion(s) to 1 file(s)CHANGELOG.Tests.Thread `Atomic` side-condition through `ElimModal`, `ElimAcc` and `ElimInv`.Merge branch 'robbert/heap_lang_tweaks' into 'master'Apply 1 suggestion(s) to 1 file(s)Remove framing for fractional.ci/robbert/fram…ci/robbert/frame_fractionalMake use of better `iMod` for updates.robbert/fupd_elimrobbert/fupd_elimGeneralize `elim_modal_fupd_fupd` to handle different masks.Add lemmas `fupd_(intro_)?mask_subseteq` and `fupd_intro_mask_eq`; rename `fupd_mask_same` into `fupd_mask_eq`.Remove old FIXMEs.ci/robbert/coq_…ci/robbert/coq_bug_7773Fix typo.CHANGELOG.Move HeapLang `head_step` tactics and `Atomic`/`PureExec` instances to their own files.Put heap_lang tactics in better order.`Free` is atomic.Merge branch 'internal-eq-timeless' into 'master'Drop line breakMerge branch 'ci/robbert/hint_extern_impl_persistent' into 'master'Remove old `Hint Extern` hack for `impl_persistent` that seems no longer needed.Merge branch 'robbert/issue/393' into 'master'CHANGELOG.Fix issue #393: repair statement of `fupd_plainly_laterN`.Merge branch 'bump-stdpp' into 'master'Bump std++ (macOS build fix)add mono_nat_auth_lbBetter links in CHANGELOG.Merge branch 'ralf/singleton_mono' into 'master'Merge branch 'persistent-points-to-2' into 'master'add singleton_monoImprove CHANGELOG.Add some FIXMES.