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.04Jan3128Dec272623222120191817161514131211987652130Nov2928272625242322212019181716151098765432131Oct302827262522211817161514131210976543228Sep272120191514131298765432131Aug302928272625242322Tweak 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.Tweak core.vcore: fix typo in lemma namefewer linebreaks in the coreImplement JH's idea of a "core of an assertion"fix buildmove gen_heap to base_logic. It does not depend on WP or antyhing language-specific.ssreflect 1.6.1 is out :)uPred entailment commutes over limitsFix issue #54.show na_own_accfix an error message in iInductionshow lemma about big_sepL and zip_withadd decide_left, decide_rightCI: script spacingfix coq 8.6 CI job name