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.026May252423222120191716151312987642130Apr29272625242317169873229Mar26222019171615141312765432128Feb2726252423222120191816137653130Jan2928272625242322191817161514131110225Dec22212019181514131210876330Nov29282726232220161211986131Oct292726252422212019181312111075432130Sep27262019181210331Aug3029241713112131JulGeneralize `frac_auth_frag_discrete` to `≠ 1` fraction.Merge branch 'ralf/subg' into 'master'Merge branch 'master' of https://gitlab.mpi-sws.org/iris/iriscomment why we disable warningsMerge branch 'ci/robbert/more_248' into 'master'Relax subG modeMore simple changes to make proof mode terms more compact.rewrite build-all in pythonpair_validMerge branch 'iInv_more_args' into 'master'Allow up to 10 introduction patterns for iInv.Merge branch 'auth_rename' into 'master'More renameMerge branch 'ci/joe/compact_ipm_simple' into 'master'Fix error message regression, add new test cases.Fix spacingAdd more renamesAdd renaming for to CHANGELOGMerge branch 'robbert/auth_consistency_fixes' into 'master'More consistent naming for `auth`.Merge branch 'frac_auth' into 'master'Make authoritative part of auth fractionalRevert spurious change to ref file.ci/joe/compact_…ci/joe/compact_ipm_simpleRemove context duplication from tac_exist_destruct.Delete some context duplication in iInv.Fix error message in iOrDestruct.Fix error handling of iPoseProofCoreHyp.More stylistic fixes.Fix another typo in proofmode.Fix style issues in compact IPM changes.Fix error message regression, add new test cases.Fix build on Coq master.Convert remaining simple tactics.Covert tac_pose_proof.Delete extra copies of context from terms for some proof mode tactics.Fix typo.Merge branch 'ci/robbert/faster_iFresh' into 'master'expand CHANGELOGtest 8.9.1, no longer test 8.7.1, 8.8.0Fix compilation with Coq master.