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.017May1514111098743230Apr2928272625242322212019181211109654331Mar30282724222120191716151413121198765432128Feb27262524232221201918161514131298763231Jan302927252423222120191816131211107331Dec3029232221clean up test tmpfile; remove .vo if test failed so it gets re-runfix test suite makefile to work with Coq mastermake clean should clean the tests directory if it existsmove test suite out of theories/ so it does not get installed; also check output of test suite so that we can test printingMerge branch 'master' into gen_proofmodeMove generic `IsOp` instances to `algebra/proofmode_classes.v`.`IsOp` instance for singleton map.Rename `frag_auth_op` into `frac_auth_frag_op` (the old name was inconsistent).Merge branch 'ralf/inv' into 'gen_proofmode'Fix typo.False is affine.Merge branch 'master' into gen_proofmodeBump std++.use m as prefix for things of option typemake a proofmode copy of from_option to control simplificationMerge branch 'master' into 'master'Bump Mtac commit. [On master again.]Bump Mtac commit. [Off-master again; constr stuff.]All multiset elements are cancelable.Some results about `frac_auth` by Danny and Ales.Misc monPred tweaks.update CI/Makefilefix make build-depupdate CIBump Mtac commit.Bump Mtac commit. [Back on master.]fix iPureIntro when the goal is an absorbing modalitylemmas about □?p P and <affine>?p PBump Mtac commit. [Off-master, constr stuff.]Bump Mtac commit. [Off-master, constr stuff.]Merge branch 'ralf/löb' into 'gen_proofmode'extend Löb proof commentSmall tweaks to `weak_löb`.Shorten 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_proofmode