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.08Jan76543128Dec272623222120191817161514131211987652130Nov2928272625242322212019181716151098765432131Oct302827262522211817161514131210976543228Sep272120191514131298765432131Aug3029282726fix 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 proofdisable annoying warningMerge branch 'list_renaming_stuff'Recursive [inv_vec].Renaming in prelude/list.more restrictive Proof Using hints in (most files of the) preludemore restrictive Proof Using hints in base_logic, algebramore restrictive Proof Using hints in heap_lang, proofmode, testsfix CI testing for axioms in build outputprogram_logic: improve 'proof using' hint to be more minimal, more future-proofMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqAdd lemma compl_chain_map.a little theory about limit preservation"Proof using" hints for agree.vMerge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqdocument base_logic.upredtweak sigma COFEfix the build even moreapply feedback; fix compilation with coq 8.5Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqCOFE for sigma typesFix typos.Fix links in README.Refactor proofs for invariant opening.eauto hint for introducing ◇.Tweak some proof using tweaks for setoid stuff.tune "Proof using" directives to minimize differences to previous types of all lemmasalgebra.sts as the wrong file, the affected lemmas are in base_logic.lib.sts (already fixed by Robbert)Let iRevertIntros ensure that we are in the proofmode.Missing stuff in Proofmode.md.Get rid of a SearchAbout.Tweak lib/sts so not all lemmas are parametrized by φ.don't use Proof Using in a few files that get too many unnecessary annotations from thisMerge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq