Skip to content
Snippets Groups Projects
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/iFrame
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/naive_solver
  • 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
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.03Apr2131Mar272523212019181613121096428Feb26252423212019181716151413121110765432130Jan29242321181716151413111098720Dec19181413109654225Nov222120141312111087652131Oct2522181412119630Sep292826252320191413121198630Aug292827262524221614131298765131Jul30292214131297532130Jun2928272625add pair_included, auth_frag_core, singleton_core_totalralf/rename_op_…ralf/rename_op_coremake direction and names of more `f_op`/`f_core` rewrite lemmas more consistentupdate dependenciesmastermasterCHANGELOG.robbert/lock_na…robbert/lock_namespaceRemove namespaces from lock API.Add `NonExpansive` instances for `!!!` on maps and lists.CHANGELOG.robbert/telerobbert/teleAdd proof mode test cases for handling telescopes.Support telescopic `∀..` in `iStartProof`.Add affine, absorbing, persistent, and timeless instances for telescopes.Missing proof mode instances for telescopes.Consistently Use meta variable `TT` for telescopes in `class_instances_bi`.Merge branch 'robbert/oFunctor' into 'master'CHANGELOG.Add `{o,r,ur}Functor_oFunctor_compose` to compose two functors.Rename `{o,r,ur}Functor_{ne,id,compose,contractive}` intoMerge branch 'robbert/lock_contractive' into 'master'Merge 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'