Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • R RT-PROOFS
  • Group information
    • Group information
    • Activity
    • Labels
    • Members
  • Issues 16
    • Issues 16
    • List
    • Board
    • Milestones
  • Merge requests 4
    • Merge requests 4
  • Packages and registries
    • Packages and registries
    • Package Registry
Collapse sidebar
  • RT-PROOFS
  • Merge requests
  • Open 4
  • Merged 237
  • Closed 32
  • All 273
  • note some of GEL's generalizing properties
    rt-proofs!274 · created Mar 23, 2023 by Björn Brandenburg
    • MERGED
    • 18
    updated Mar 24, 2023
  • fix `make vacuum` if no `_CoqProject` is present
    rt-proofs!273 · created Mar 23, 2023 by Björn Brandenburg
    • MERGED
    • 1
    updated Mar 23, 2023
  • Bump MathComp lower bound to >= 1.16.0 and Coq to >= 8.16.
    rt-proofs!272 · created Mar 17, 2023 by Pierre Roux
    • MERGED
    • 5
    updated Mar 17, 2023
  • Put mangle-names in a separate CI target
    rt-proofs!271 · created Mar 16, 2023 by Pierre Roux
    • MERGED
    • 1
    updated Mar 16, 2023
  • Add a CI target testing mangle names
    rt-proofs!266 · created Mar 01, 2023 by Pierre Roux
    • MERGED
    • 1
    updated Mar 16, 2023
  • Use mathcomp's int instead of stdlib's Z
    rt-proofs!259 · created Feb 17, 2023 by Pierre Roux
    • MERGED
    • 10
    updated Mar 16, 2023
  • Move interference definitions out of ideal/iw_instantiation.v
    rt-proofs!264 · created Feb 27, 2023 by Pierre Roux
    • MERGED
    • 13
    updated Mar 16, 2023
  • ELF Definition
    rt-proofs!270 · created Mar 13, 2023 by Meenal Gupta
    • MERGED
    • 76
    updated Mar 15, 2023
  • priority relations and conversions for fp and jlfp
    rt-proofs!268 · created Mar 03, 2023 by Meenal Gupta
    • MERGED
    • 43
    updated Mar 13, 2023
  • also spell-check *.md files
    rt-proofs!267 · created Mar 02, 2023 by Björn Brandenburg
    • MERGED
    • 0
    updated Mar 04, 2023
  • Add a warning about implicit arguments in guidelines
    rt-proofs!260 · created Feb 17, 2023 by Pierre Roux
    • MERGED
    • 9
    updated Mar 02, 2023
  • Factorize two proofs
    rt-proofs!262 · created Feb 24, 2023 by Pierre Roux
    • MERGED
    • Approved
    • 2
    updated Feb 28, 2023
  • Rewrite create_makefile.sh as a Makefile
    rt-proofs!263 · created Feb 27, 2023 by Pierre Roux
    • MERGED
    • 2
    updated Feb 28, 2023
  • Fix implicit arguments in model/priority/classes.v
    rt-proofs!258 · created Feb 16, 2023 by Pierre Roux
    • MERGED
    • Approved
    • 1
    • 11
    updated Feb 27, 2023
  • Split OPAM packages
    rt-proofs!257 · created Feb 14, 2023 by Pierre Roux
    • MERGED
    • 5
    updated Feb 14, 2023
  • coding-guideline changes
    rt-proofs!255 · created Feb 13, 2023 by Meenal Gupta
    • MERGED
    • 13
    updated Feb 14, 2023
  • [CI] Don't recompile mathcomp solvable and field
    rt-proofs!256 · created Feb 14, 2023 by Pierre Roux
    • MERGED
    • 1
    updated Feb 14, 2023
  • More qualified import of mathcomp.zidfy.ssrZ
    rt-proofs!254 · created Jan 28, 2023 by Lasse Blaauwbroek
    • MERGED
    • 0
    updated Jan 29, 2023
  • Generalize ideal aRTA
    rt-proofs!116 · created Sep 14, 2020 by Sergey Bozhko
    • MERGED
    • Approved
    • 173
    updated Jan 23, 2023
  • Retire classic Prosa
    rt-proofs!253 · created Nov 10, 2022 by Björn Brandenburg
    • MERGED
    • 0
    updated Nov 11, 2022
  • Prev
  • 1
  • 2
  • 3
  • 4
  • 5
  • …
  • 12
  • Next