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/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
Created with Raphaël 2.2.08Feb763231Jan2927252423222120191816131211107331Dec30292322212019181514131211108765432130Nov292827262423222120181615141312119876543231Oct30292827262524232019181210975429Sep28272625242120Bump stdpp.Document BI axioms in terms of the axioms in the ordered RA model.Note that `plainly` will be removed from the BI interface.Merge branch 'robbert/iFrame_improvements' into 'master'Bump stdpp and fix the CI (hopefully).Merge branch 'robbert/super_iAlways' into 'gen_proofmode'Tests for framing under conjunctions.Frame in both sides of a conjunction.Support framing under implications.Some test cases/uses for stronger framing in disjunctions.Better framing support for disjunctions.Test case for `iAlways` and the `absolutely` modality.Support `absolutely` modality in `iAlways`.Write some documentation about the new `iAlways` tactic.Generic `iAlways` tactic.Fix notation scopes of `absolutely` and `relatively`.More consistent names for `mono` lemmas for `absolutely`/`relatively`.Add lemmas about relatively and absolutely.Fix Absolute instances.Cleanup Absolute type class.Absolute type class, and new names for absolutely and relatively.CI: build against coq master instead of 8.7.dev branchstop overwriting make uninstallstop overwriting make uninstallMove internal_eq in the sbi interface.Bump stdpp version.Fix typo.Docs: fixpoints only exist when the type is inhabited.Bump stdpp.update emacs snippetSupport framing pure facts and equalities under an embedding.Add test.Make it possible to introduce an hypothesis which is behind an embedding.Define monPred_ex and monPred_all in terms of the embedding, for better support in the proof mode.Make iStartProof convert Coq universals into bi universals.Make sure all the itactics fail if the do not go through the proof mode.Move the AsValid typeclass in classes.v and class_instances.vdocument editor configuration for unicode input/outputMerge branch 'robbert/invariant_weaken' into 'master'Show that non-atomic invariants are closed under logical equivalence.