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.024May23222120191716151312987642130Apr29272625242317169873229Mar26222019171615141312765432128Feb2726252423222120191816137653130Jan2928272625242322191817161514131110225Dec22212019181514131210876330Nov29282726232220161211986131Oct292726252422212019181312111075432130Sep27262019181210331Aug3029241713112131Jul24231918Merge 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.Merge branch 'declare-ipreprop-cofe' into 'master'Fix build on Coq master.ci/joe/compact_…ci/joe/compact_ipmRevert "Remove redundant pm_reduce." and "Commute match with implication in tac_frame."Remove redundant pm_reduce.Commute match with implication in tac_frame.Convert other tac_specialize* to avoid nested conjunctions.Switch back to notypeclasses refine on tac_specialize*Remove unneeded pm_reduce.Swap implication with match in some of tac_specialize*.Try to improve performance of converted tac_specialize_*Convert remaining tac_specialize_* lemmas.Convert tac_specialize frame.Convert tac_specialize_assert.