Skip to content
Snippets Groups Projects
Select Git revision
  • ci/3.1.0
  • ci/debug
  • ci/disable-ltac-backtrace
  • ci/for_proph
  • ci/janno/debug-opam
  • ci/janno/let_bind_envs
  • ci/janno/vmcast
  • ci/joe/compact_ipm
  • ci/joe/compact_ipm_remaining
  • ci/joe/compact_ipm_simple
  • ci/maximedenes/instance-nobody-open-proof
  • ci/msammler/iris-coq-seal_big_opM
  • ci/mtac2-tt
  • ci/prophecy
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/ralf/set_unfold_elements
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • 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
31 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.07May43230Apr2928272625242322212019181211109654331Mar30282724222120191716151413121198765432128Feb27262524232221201918161514131298763231Jan302927252423222120191816131211107331Dec3029232221201918151413Shorten proof.Do not use automatically generated name.Bump Mtac commit. [Still off-master.]Bump Mtac commit. [Off-master again.]all SBI must be a COFEDon't create `<pers>` modalities in `iSplit` when the BI is affine.Merge branch 'gen_proofmode' of gitlab.mpi-sws.org:FP/iris-coq into gen_proofmodeMake the behavior of `iSplit` on `P ∗ □ Q` consistent with that of `iDestruct`.Fix `Hint Mode` of `IntoAbsorbingly`.Derive löb induction from later introductionfactor out entails_eq_True as its own lemmaMerge branch 'master' into gen_proofmodefix `head_stuck`generalize proofmode accessors to work with all modalities, and not depend on SBI or FUpd any morerename AccElim -> ElimAccmake the ElimAcc instance for WP add a view shiftElimInv generalized to any BI actually works fineAdd support for ElimInv to introduce a binder from the accessorUse new `mrun_static` tactic to avoid dyn. checks.Bump Mtac commit.Bump Mtac commit. [Back to master.]Bump Mtac commit. [Still on temporary branch.]Bump Mtac commit. [Still on temporary branch.]Bump Mtac commit. [Still on temporary branch.]Bump Mtac commit. [Still on temporary branch.]Bump Mtac commit. [Still on temporary branch.]Bump Mtac commit. [Still on temporary branch.]Bump std++.Fix #184.Bump Mtac commit. [Still on temporary branch.]Bump Mtac commit. [Still on temporary branch.]I think I made the previous commit in the wrong project... anyway, bump std++bump IrisBump Mtac version. [Still on temp. branch.]Temporarily use non-master branch of Mtac2.have two instances for ElimInv and MakeEmbed, instead of one horrible oneBump Mtac version.New IntoAcc typeclass to decouple creating and elliminating accessors; ElimInv supports both with and without Hcloserename InvOpener -> AccElimaccessor-style iInv without Hclose