Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 185
    • Issues 185
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 19
    • Merge requests 19
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Artifacts
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Model experiments
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Repository
  • Branches
  • Overview
  • Active
  • Stale
  • All
  • ci/name-mangle
    46e8f68d · enable name mangling · Sep 29, 2023
    Download source code
    zip tar.gz tar.bz2 tar
  • ci/timing
    4abdc826 · timing with Coq 8.17 · Sep 29, 2023
    Download source code
    zip tar.gz tar.bz2 tar
  • master default protected
    4f3a385f · add 'iris-bot timing all' · Sep 29, 2023
    Download source code
    zip tar.gz tar.bz2 tar
  • robbert/lock_G_Σ
    fa555c7b · Test that lock `Σ`s can be found in adequacy. · Aug 29, 2023
    !980
    Download source code
    zip tar.gz tar.bz2 tar
  • robbert/internal_fractional_tweaks
    8de85872 · Style tweaks to rwlocks. · Aug 28, 2023
    !976
    Download source code
    zip tar.gz tar.bz2 tar
  • ralf/ra-infer
    bd80b71c · experiment: use coq's ability to infer more canonical structures · Aug 11, 2023
    !972
    Download source code
    zip tar.gz tar.bz2 tar
  • ralf/iso_cmra
    8ecf601f · generalize iso_cmra_mixin_restrict to a lemma that can also restrict the domain · Aug 10, 2023
    !970
    Download source code
    zip tar.gz tar.bz2 tar
  • ralf/fmap_dist_inj
    8d59d7a5 · add option_fmap_dist_inj lemma · Aug 10, 2023
    !969
    Download source code
    zip tar.gz tar.bz2 tar
  • ralf/solve-proper-subrelation
    188132d2 · have solve_proper exploit OfeDiscrete and LeibnizEquiv · Aug 08, 2023
    !968
    Download source code
    zip tar.gz tar.bz2 tar
  • ralf/gmap_view_cmra
    b579fafb · port the rest of Iris to the new gmap_view · Jul 27, 2023
    !959
    Download source code
    zip tar.gz tar.bz2 tar
  • robbert/local_ltac_proofmode
    908ae8f9 · Avoid `Local Ltac` and `Local Tactic Notation` in proofmode. · Jul 24, 2023
    !953
    Download source code
    zip tar.gz tar.bz2 tar
  • robbert/sbi
    009bbd9b · Remove useless `BiAffine` premises for `Plain` of big ops. · Jul 09, 2023
    Download source code
    zip tar.gz tar.bz2 tar
  • coq-bugs/tc-resolution-cannot-unify-with-self
    a1abaf74 · reproducer for Coq bug · Jun 04, 2023
    Download source code
    zip tar.gz tar.bz2 tar
  • ci/robbert/hint_cut_plain
    df44c4fe · Use `Hint Cut` for `Plain`. · May 05, 2023
    Download source code
    zip tar.gz tar.bz2 tar
  • robbert/hint_cut_plain
    df44c4fe · Use `Hint Cut` for `Plain`. · May 05, 2023
    Download source code
    zip tar.gz tar.bz2 tar
  • ci/ralf/options-timing
    39e22b1f · Revert "re-export std++ options" · May 05, 2023
    Download source code
    zip tar.gz tar.bz2 tar
  • ci/hint-cut-revert
    4069e553 · Revert "Merge branch 'ralf/separable' into 'master'" · May 05, 2023
    Download source code
    zip tar.gz tar.bz2 tar
  • robbert/pm_unify_class
    221ce5ec · `Unify` type classes that factors out use of `notypeclasses refine` in proof mode classes. · Apr 30, 2023
    !916
    Download source code
    zip tar.gz tar.bz2 tar
  • ralf/bi-persistently-emp
    220dad25 · Change `BiPersistentlyEmp` into `BiPersistentlyTrue`, which seems more natural. · Apr 28, 2023
    Download source code
    zip tar.gz tar.bz2 tar
  • robbert/resolve_tc
    9fe5d81c · Use `resolve_tc` and remove all uses of "legacy" `apply` in Iris Proof Mode. · Apr 18, 2023
    Download source code
    zip tar.gz tar.bz2 tar
  • Prev
  • 1
  • 2
  • 3
  • 4
  • 5
  • Next