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.09Jan876543128Dec272623222120191817161514131211987652130Nov2928272625242322212019181716151098765432131Oct302827262522211817161514131210976543228Sep272120191514131298765432131Aug302928let 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 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 φ.