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.03Jan128Dec272623222120191817161514131211987652130Nov2928272625242322212019181716151098765432131Oct302827262522211817161514131210976543228Sep272120191514131298765432131Aug302928272625242322212019timing: 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 namebuild against the released Coq 8.6Support sequential languages.swasey/sequentialswasey/sequentialAdd progress bit to wp (and slightly generalize wp_step, wp_safe).Revert git:00444b0 as the weaker notion of atomicity is too weak for unsafe WP.make ndisj hints look through definitions to unfold more stuffMerge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqfix assigning priority to ndisj hintMove stuff out of sections that does not depend on the section variables.Simplify proofs relating nth to lookup.proofmode: show that quantifiers preserve puritylist: relate nth and lookup