Skip to content
Snippets Groups Projects
Select Git revision
  • atomic
  • ci/3.1.0
  • ci/debug
  • ci/janno/debug-opam
  • ci/janno/vmcast
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/robbert/into_val_pures
  • ci/stability
  • ci/value_constructor
  • fast_string
  • fix-class-apply
  • fix-export
  • fix-from-assumption-exact
  • fix-local-inductive
  • instance-nobody-open-proof
  • iris-3.0
  • iris-3.1
  • janno/metacoq
  • jh/done_contradiction
  • 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
30 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.08Aug6542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar29232221201918171615141211Merge 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 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-coq