Skip to content
Snippets Groups Projects
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
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.017Jan131211109876543128Dec272623222120191817161514131211987652130Nov2928272625242322212019181716151098765432131Oct302827262522211817161514131210976543228Sep272120191514131298765Add examples of IPM paper to tests/ipm_paper.v.avoid re-downloading already properly pinned packagesdo CI in 3.0 branchthe Coq OPAM package is fixed, no need to install ocamlfind manually any moreMerge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqtry to clarify adequacyfix adequacy stmtSupport upto 12 variables in iIntros.Simplify definition of WP.Remove spurious constRF.Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqdocs: fix adequacy for state invariant-style WPRenaming again [na_inG] and adding [na_invΣ] and [subG_na_invG].Remove some FIXMEs: Coq bug 4762 has been fixed in 8.6.Remove FIXME that is no longer needed in current 8.6.Use lazymatch in reshape_val, it should not backtrack.Correct a bug in reshape_expr.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqRename tl_inG into na_inG.Merge branch 'coq-8.6' into 'master' Mark notation as "only printing"Use primitive projections for sealinguse coq 8.6 mode '!' to fix diverging apply:no longer test on or support Coq 8.5this is Iris 3.0.0!iris-3.0.0iris-3.0.0CHANGELOG: list things have been renamedMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqawk.Makefile: uninstall .v and .glob filesawk.Makefile: uninstall: also delete empty directoriesfix awk.Makefileupdate awk.Makefilelet solve_inG handle higher-arity functions for the \Sigmaadd a tactic to automatically solve goals that show inG from subGfix vio2vo patched targetMake instances EqDecision and Countable of gmultiset less eager.typomake Makefile work with POSIX awkpatch vio2vo target to only rebuild outdated .vo filesadd \Sigma for boxes; use a coercion for constant functorssimplify an inG proof
Loading