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/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
  • ci/robbert/into_val_pures
  • 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.04Jul3230Jun2928262523222120191817161514131211109876543131May302928272524232018171514111098743230Apr2928272625242322212019181211109654331Mar30282724222120191716151413121198765432128Feb2726252423222120Split prettification from proof mode reductionremove big_opL from prettification listmake `wp_alloc l as "?"` behave as expectedchangelogMerge branch 'ci/ralf/telescopes' into 'gen_proofmode'Move laterN_iter to derived_laws_sbi, because it's more generic.make sbi_laterN compute and rely on that instead of MakeLaterNadd some more printing to some testsconsistently use pm_prettify for post-tactic simplificationrely on normalization for laterNralf/later-normalralf/later-normalproofmode: normalize big_opLtest and fix more telescope normalizationfix nitsadd general telescopes and telescopic BI binders and proofmode supportmake pm_maybe_wand a BI connective; reduce BI connectives and option combinators in the proofmode with cbnMerge branch 'ralf/cas' into 'gen_proofmode'add wp_cas tactic that performs case distinction; weaken logatm heap to be easier to usemake README ready for mergerCHANGELOGAllow comparing even more values in CAS by making things more consistentwe can allow comparing more things -- and explain whyMerge branch 'master' into gen_proofmodebump std++Bump std++.More Implicit Types.bind scope before defining notation, to make sure the scope is set for the notationdocs: Fix definition of validity for authallow comparing more things in CASdocs: fix typoMerge branch 'ralf/cas' into 'gen_proofmode'test 'not a CAS' error message as wellwp_cas_fail/succ: Report error when proving vals_cas_compare_safe; fast_done is enoughmove option notation to lang.v so we can use it to define CAS compare safetyMake CAS slightly more realisticMAKE_REF overwrites COQ_BROKENdon't check output on testsuite at all when running against 8.9prove a variant of wp_invariance that does not require finding fupd_intro_mask'bump std++; test that we don't break setoid_rewritealways use notypeclasses refinebump std++