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.06Aug542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar29232221201918171615141211Try 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 allocationRemove duplicate iVs and iVsIntro tactic.start proving Derek's contradictionAdd missing file program_logic/iris.More introduction patterns.Iris 3.0: invariants and weakest preconditions encoded in the logic.Use rvs in counter_example and integrate with adequacy to obtain False.Stronger soundness lemmas for uPred.Merge branch 'master' into iris3.0Define uPred_now_True P := ▷ False ∨ P.Remove FIXME.Make iApply more powerful and uniform.show that even \later^n False is inconsistent (for any fixed n); properly use pvs in counter_examplesMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqshow that having saved propositions without a \later is inconsistentfix some typos in the docsBetter lemmas for splitting the fractional heap_mapsto.Injectivity instance for Z.of_nat.