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.01Apr31Mar272523212019181613121096428Feb262524232120191817151413121110765432130Jan29242321181716151413111098720Dec19181413109654225Nov222120141312111087652131Oct2522181412119620Sep19131198630Aug2928272625242216141312987630Jul221413129753130Jun292827262524212019181716151413121110CHANGELOG.Rename `{o,r,ur}Functor_diag` into `{o,r,ur}Functor_apply`.Kill `{o,r,ur}Functor_diag` coercions.Remove spurious space.Merge branch 'robbert/iso' into 'master'Some Coqdoc improvements in the OFE file.CHANGELOG.Make use of OFE isomorphisms in COFE solver.Add notion of isomorphism between OFEs.these are all functors from OFEsmention which categories these functors map to whichMerge branch 'inj-typeclass-2' into 'master'Revise uses of `inj` from !408 as discussedProve that `≡` is limit preserving.Let `iNext` detect equalities `Next x ≡ Next y`.Merge branch 'inj-typeclass' into 'master'Replace explicit use of Inj instances by injMerge branch 'msammler/fix_drop_insert' into 'master'drop_insert -> drop_insert_gtMerge branch 'add-missing-proof' into 'master'Add missing `Proof.` to sealing proofsMerge branch 'spell-check' into 'master'Spell check proof_guide.mdMerge branch 'sbi-eq-notation-sections' into 'master'sbi_internal_eq: add "sections" of notation, following stdppMerge branch 'robbert/atomic_wp_seq_step' into 'master'Prove stepping (i.e., non-value) version of `atomic_wp_seq`.Merge branch 'robbert/exist_laterable' into 'master'Prove `Laterable (∃ x, Φ x)`.Remove redundant space.Merge branch 'vscode-editor-docs' into 'master'Add VS code to the editor.md docsMerge branch 'robbert/iAssumption' into 'master'Add documentation.CHANGELOG entry.Make `iAssumption` work on `⊢ ...` premises in the Coq context.Fix errors of `iAssumption`, `iExact`, and friends.Fix bad line break.Instance for `Affine (□?p P)`.update dependencies
Loading