Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • ci/debug
  • 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/msammler/iris-coq-seal_big_opM
  • ci/ralf/pm_red
  • ci/ralf/retime
  • ci/ralf/set_unfold_elements
  • ci/ralf/transfinite
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/naive_solver
  • ci/robbert/set_unfold
  • 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
31 results
Created with Raphaël 2.2.09Aug86542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar29232221201918171615141211Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqParentheses.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqInhabited instance for any Empty instance.make the two proofs of contradictions more similar to each othertypo fixesBetter fix to avoid relying on the order in which simplify_eq works.start writing a CHANGELOG for Iris 3.0Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqBetter 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.