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.08Aug6542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar29232221201918171615141211Better Coq 8.6 compatibilityGeneralize the Iris language to forking off multiple threads.Extensionality property for fmap on lists in terms of dist.Remove gFunctorList and use gFunctors everywhere.Fix TODO in counter_examples.Some general stuff about fin.Omit hypothesis name from many proof mode errors.Revert "Iterated later modality."Remove some useless uses of upred_tactics.Simplify now_True_rvs.New test case: counter with explicit CMRA construction.counter_example: Turn a comment into a proper TODOexplain how the ghost state for the counter example can be implementedMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqFix building with ssreflect 1.6Fix compatibility with ssreflect 1.6 (which is used on the CI machine).Assert that we have only one goal (debugging CI failure)Try the ssreflect apply at the place the CI builder fails.Add missing heap_lang/adequacy.Restore program_logic/viewshifts.Rename the wp_focus tactic into wp_bind.Improve error messages of iSplitL and iSplitR.Document why cofe_fun is a definition.No longer break now_True abstraction.Generalize iTimeless to deal with now_True hypotheses.More now_True laws.Simplify the counter example proof a bit.Turn some foralls into unicode foralls.Merge branch 'iris3.0' of gitlab.mpi-sws.org:FP/iris-coq into iris3.0Append on gFunctorList.A nicer version of adequacy of Iris and specialize it to heap_lang.Make wp_strong_mono stronger and use it to prove wp_pvs.Clean up Imports so that the ={E}=★ notation is displayed properly.Better error message when iVs is used in non-view shift goal.fix a commentvastly simplify the counterexamplecounterexample no longer needs duplicable ghost stateMerge branch 'iris3.0' of gitlab.mpi-sws.org:FP/iris-coq into iris3.0complete proof that invariants without laters are inconsistentwe don't need no self-referential invariant allocation