Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • atomic
  • ci/3.1.0
  • ci/debug
  • ci/disable-ltac-backtrace
  • ci/janno/debug-opam
  • ci/janno/let_bind_envs
  • ci/janno/reduction_no_check
  • ci/janno/vmcast
  • ci/joe/compact_ipm
  • ci/maximedenes/instance-nobody-open-proof
  • ci/prophecy
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/ralf/set_unfold_elements
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/set_unfold
  • ci/robbert/tc_opaque
  • ci/stability
  • ci/value_constructor
  • 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
Created with Raphaël 2.2.024Aug2322212019181716141110986542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120191312111097643229Apr272625242120191815141312111098730Mar29232221201918Generalize proof mode type class IntoSep.Move some lifting specific tactics to lifting.v.Remove old tests about heap_lang reductions.Persistence of invariant in wp_invariance is not needed.Tweak wp_invariance.Prove adequacy of observational view shifts.Generalize equality of heap_lang so it works on any value.Some thread_local tweaks.Do not use [ucmraT]s as argument of inG.Simplifying thread local invariantsNow really get rid of the eq_rect_eq axiom.Prove UIP for decidable types without relying on the stdlib.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coquse Psatz without using axioms about real numbersSimplify proof of fixpoint_unique.Prove uniqueness of Banach's fixpoint.docs: mention uniqueness of fixed-pointsdocument that units no logner have to be concreteRemove the requirement that the unit of a CMRA is timeless.Import less Program stuff to avoid UIP/fun_ext showing up with coqchk.CI: fix running coqchkdocs: fix typo in pre-wpdo "Print Assumptions" outside of sectionsCI: run make verifymake coqchk happy with prelude.prettyfix calling makefile on specific filesUSeless spacesMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqThread-local invariants.docs: fix another typoadd some redundant parensMake coqchk slightly happier with prelude/prettyMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqFix use of undefined universe "U"Merge branch 'master' into 'master'Merge branch 'master' into 'master' Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdocs: fix typo in namespacesRemove old branch from gitlab-ci.ymlMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq