Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/robbert/big_op_binder
  • 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
  • iris-4.0.0
  • iris-3.6.0
  • 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
36 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.01Jul30Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar292322212019181716151412111098765432129Feb2827262524Improve 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.Some clean up.Oops!Move some proof mode classes to their own file.Define discreteUR constructor.Remove useless type class instance.Revert "Counting CMRA" because it is already in cmra.v (called natR).Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqRename type classes in proof mode.Move class for later stripping to proofmode.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqCounting CMRAImprove solve_proper a bit.Fix inconsistent name later_exist'.Make iSplit work with later and always.Rename uPred_const -> uPred_pure.Use type classes instead of option hack to remove Trues while framing.Generalize 7c4416b6 to remove head "value ;;" expressions after any wp_ tactic.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqadd some comments explaining design decisionsTactic iSimplifyEq that substitutes Leibniz equalities that are in the proof mode context.Let wp_store to a wp_seq if possible.heap_lang notations for Some/None.Remove wp_case, add wp_match.More hlist stuff.Replace some non-unicode arrows.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqInclude jh_simplified_ressources in the CI branches
Loading