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.029Oct2827262524232019181210975429Sep282726252421201918171615141198628Aug262423222120181776428Jul14121027Jun13128625May1712927Apr261913121175431Mar302824232221201615141211109765124Feb23222120181716151413121110987632130Jan2928272625242322212017131211109876543128Dec2726232221201918171615141312State `internal_eq_rewrite` in the logic.Merge branch 'jh/bottom_notation' into 'master'Notation for disjointness: replace ⊥ with ##, so that ⊥ can be used for bottom.opam CI: more verbose output; more robust opamopam-ci: silence accidental outputactually, it's called Coq 8.7.0fix Coq version numbertest agains release Coq 8.7 and ssreflect 1.6.2more CHANGELOGtweak CHANGELOGRevert "Temporarily remove a test that fails in Coq 8.6. See #108 for details."Bump std++.Temporarily remove a test that fails in Coq 8.6. See #108 for details.Add `FromForall` instance for `not`. This fixes issue #108.expand changelogbump std++Add note about iIntros/iAlways to CHANGELOG.Make more use of the `direction` enum in the proof mode tactics.Tweak the proof mode docs.Support `->` and `<-` for pure equalities in proof mode intro patterns.document iAlwayschangelog and commentsMerge branch 'naught' into 'master'Plain instances for the big ops.core: don't use the turnstile inside the logicPort the core to use the plainness modality and prove it is non-expansive.Proofmode support for introducing the plainness modality.Plainness and persistence of implications and wands.Simplify soundness of the base logic.Proof mode instances for eliminating plain basic updates.Proof mode instances for the plainness modality.Avoid exponential proof search due to Plain → Persistent instance.Derived rules of the plainness modality.Add the plainness modality to the model of the base logic.Removed a stray proof mode lemma.Put heap_lang's let/lambda/rec at level 200.Some updates to the CHANGELOG.list more renamingsexpand changelogdon't try to be smart about having an up-to-date opam