Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/ralf/frame-frac
  • ci/robbert/contractive_ne
  • ci/robbert/coq_bug_7773
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/frame_fractional
  • ci/robbert/iFrame
  • ci/robbert/into_fupd
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/mapsto_persist
  • ci/robbert/merge_sbi
  • ci/robbert/naive_solver
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • 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
34 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.05Jul432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765432129Feb2827262524Rename fallthrough (instances) into default.Write some proof mode documentation.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq Get rid of phi predicates everywhereFix instance for ndisjoint.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqfix a weird typoCorrectness of monotone counter.Persistence of auth_own.Give the left instance of FromAnd (P1 ★ P2) P1 P2 precedence.Notation for max and min.Mononicity of auth_own.CMRA on nat with max as op.Qp is inhabited.Lifting lemmas : get rid of \phi when it has became uselessLifting lemmas : make the initial state appear under an existential under the view shift. This is still sound, but slightly more expressive.Add lemma pure_iff.Ensure that solve_ndisj "solves", it either succeeds or fails.Use ndot_ne_disjoint more eager so it expands definitions.Local update for natLocal updates for sumsMerge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqMake Program obligations Transparent by default.New lemma : cmra_update_valid0. This let us prove a FP update using the additionnal hypothesis that the source is valid at step 0.New lemma aboud maps : fmap_deleteClean up some ndisjoint stuff in the proofmode tactics.Tweak tests/one_shot.Improve ndisj hint database.Hack to avoid getting String.length instead of List.length.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqSome properties of imapEnable $-prefixes in ssr-like {H1 .. Hn} intro-patterns to perform framing.Simplify spec_patterns parser by using a mutual fixpoint.Bring back wp_bindiCreate eauto hint for iPvsIntro.Add wp_value_pvs' (like wp_value').Fix order of imports.Make all the wp stuff (lemmas and tactics) preserve view shifts.Split IsPure into IntoPure and FromPure.