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.02Jul30Jun2928262523222120191817161514131211109876543131May302928272524232018171514111098743230Apr2928272625242322212019181211109654331Mar30282724222120191716151413121198765432128Feb272625242322212019add 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++Merge branch 'master' into gen_proofmodeupdate CIupdate CIrerun CIci/stabilityci/stabilityrerun CIrerun CIrerun CIrerun CIrerun CIrerun CIpure timing CIrerun CIrerun CIrerun CIAdd `match_goal` wrapper around `wp_pure`.Code beautification.