Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/robbert/big_op_binder
  • ci/robbert/contractive_ne
  • ci/robbert/coq_bug_7773
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/frame_fractional
  • ci/robbert/iFrame
  • ci/robbert/into_fupd
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/mapsto_persist
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • 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
36 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.05Jan43128Dec2726232221201918161514131211987652130Nov2928272625242322212019181716151098765432131Oct302827262522211817161514131210976543228Sep272120191514131298765432131Aug3029282726252423tweak 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-coqdon't use Proof Using in a few files that get too many unnecessary annotations from thisRequire `Total R` just for the merge sort theorems that actually need it.Add a rule to alloocate an invariant and open itDocument list_remove and list_remove_list.Fix more _L lemmas.Fix persistent_dup_L.Correct stupid bug about interpretation scopes.update gitlab-extract to handle the double-CI-build (Coq 8.5 and 8.6)timing: make fewer things opaquemake "make quick" quick by adding hints about the used section variablesMake it optional that iPoseProofCore performs TC inference lazily.Apply default instance for later stripping not deep in terms.Fix issue #56.Tweak uPred core.Make sure that `iIntros "*"` uses a fresh name.Tweak entails_equiv_and.Make f_contractive more robust.Ofe and Cofe structures on vectors.Version of [fixpoint_ind] that is easier to use.Coinduction principle on fixpoints.New derived lemma : entails_equiv_and.Slices are contractive.