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.013Feb1298763231Jan2927252423222120191816131211107331Dec30292322212019181514131211108765432130Nov292827262423222120181615141312119876543231Oct30292827262524232019181210975429Sep28272625Wrong kind of comment.Merge branch 'jh/affine_frompure' into 'gen_proofmode'More doc about FromPure.Merge branch 'robbert/issue_154' into 'gen_proofmode'Make FromPure depend on an affinity parameter.Revert "Make FromPure depend on an affinity parameter."Make FromPure depend on an affinity parameter.document the RA model brieflyRestore side-condition of `iMod` tactic and `ElimModal` TC.Remove hacks that are no longer needed.Makefile: honor COQBINBump stdpp.Merge branch 'ci/robbert/no_backtracking' into 'master'Fix issue #153 by using `NoBackTrack` in the `Frame` instances for ▷.Bump 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.