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.02Apr131Mar272523212019181613121096428Feb262524232120191817151413121110765432130Jan29242321181716151413111098720Dec19181413109654225Nov222120141312111087652131Oct2522181412119620Sep19131198630Aug2928272625242216141312987630Jul221413129753130Jun2928272625242120191817161514131211Merge branch 'master' of https://gitlab.mpi-sws.org/iris/iris into master.2changelog format nitCHANGELOG.Add rule `is_lock_iff` for locks.Make `_iff` and `_alter` lemmas for invariants consistent.Prove that `is_lock` is contractive.Break some very long lines in `class_instances_bi`.Remove some useless `%I` delimeters.Merge branch 'robbert/functor_diag' into 'master'Remove `-ambiguous-paths` option.Comment about coercion.CHANGELOG.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)`.