Skip to content
Snippets Groups Projects
Select Git revision
  • adjust-focused-goal
  • atomic
  • avoid-deprecated-arith
  • byte-strings
  • bytes-ident
  • 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
  • cmra-iso
  • cmra-restrict-valid
  • coqide-unicode-config
  • dfrac-smart-constructor
  • dfrac-valid-arg
  • document-ipm-classes
  • 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.023Jul2219152119Jun109429May2819Apr16151211312Mar116542126Feb2322201615141312119654211Jan26Dec21181512109220Nov171411106130Oct2423212017161514131211987654329Sep27262114118130Aug29281110984327Jul252423222130Jun29141296542131May302819141110985432130Apr292827252419181211626Mar252319201918171097Add CHANGELOG entrypolymorphic-bipolymorphic-biRemove old universe declarationsRely on universe polymorphismMake bi polymorphic in logic and quant universesMerge branch 'gset_to_gmap_theory' into 'master'mastermasterTweak CHANGELOG.Add CHANGELOG entry for big op gset_to_gmap lemmaMerge branch 'master' into gset_to_gmap_theoryMerge branch 'robbert/iInduction_wand' into 'master'Tweak CHANGELOG.CHANGELOG.Tests.Similar to `IntoIH` and `IntoWand` instances, let `tac_pure_revert` use `MakeAffinely`.Let `into_ih_impl` generate -∗ instead of →.Merge branch 'ralf/wp_cmpxchg_fail-persist' into 'master'coqdoc, changelogMerge branch 'yusuke/big_sepX_flip_mono' into 'master'Add big_sep*_flip_mono'Tweak proof.fix wp_cmpxchg_fail when points-to is in persistent contextupdate dependenciesMerge branch 'rodolphe/dune' into 'master'Allow compiling the packages with dune.Merge branch 'robbert/iInv_error' into 'master'CHANGELOG.More suggestive error message for `iInv`.Merge branch 'robbert/remove_star_spec_pattern' into 'master'Remove the `*` specialization pattern. This pattern has been deprecated and a no-op since 2017. See !41.Merge branch 'robbert/issue_571' into 'master'Bump timeout to hopefully solve !571.add Coq 8.21 to NOREFupdate dependenciesupdate dependenciesAdd lemmas for big_opS and gmap singletonsupdate dependenciesMerge branch 'fix-doc-links' into 'master'Fix broken code links in docsfix-doc-linksfix-doc-linksbump std++exclude Coq 8.20 from printing testsMerge branch 'feat-na-own-empty' into 'master'