All pull requests

Pull requests

• Elimination constraints for bounded sort polymorphism

  #111·jrosain opened Sep 26, 2025·

  ·
  6

• Debugging generalized rewriting tactics

  #110·radrow opened Jul 7, 2025·

  ·
  1

• Multiple Default Typeclass Databases

  #109·Janno opened Jul 2, 2025·

  ·
  10

• Proof scripts indentation checking

  #108·proux01 opened Jun 30, 2025·

  ·
  38

• Asserting outputs of vernacular commands and tactics

  #107·radrow opened Jun 4, 2025·

  ·
  14

• Named notation levels

  #106·proux01 opened Jun 3, 2025·

  ·
  28

• Reduction

  #105·Janno opened Feb 13, 2025·

  ·
  18

• Rocq Package Metadata: Piggybacking on Findlib.

  #101·rlepigre opened Nov 11, 2024·

  ·
  32

• A Compilation of Short Interactive Tutorials and How-To Guides for Coq

  #91·thomas-lamiaux opened Jun 20, 2024·

  ·
  30

• Template poly redesign using sort poly

  #90·SkySkimmer opened May 21, 2024Contributor·

  ·
  12

• A unique execution path for the treatement of universes in declare.ml

  #89·herbelin opened May 20, 2024Member·

  ·
  1

• Abstract ("side effects") redesign (WIP)

  #88·SkySkimmer opened May 16, 2024Contributor·

  ·

• Reduce barriers to contributing to the standard library

  #86·andres-erbsen opened Apr 12, 2024·

  ·
  14

• Enriched and unified syntax for reduction strategies

  #85·herbelin opened Feb 9, 2024Member·

  ·
  6

• Added new CEP Symbol Sets

  #84·MSoegtropIMC opened Feb 6, 2024·

  ·
  5

• Boost stdlib development

  #83·proux01 opened Feb 6, 2024·

  ·
  159

• Rocq Object Metadata

  #80·CohenCyril opened Dec 18, 2023·

  ·
  6

• Adding a CEP about Reals

  #74·Villetaneuse opened Sep 15, 2023·

  ·
  23

• Giving access in match to the expansion of the term being matched via an alias in order to support more fixpoints

  #73·herbelin opened Aug 10, 2023Member·

  ·
  4

• Discharge on the fly

  #72·herbelin opened Jul 31, 2023Member·

  ·
  5

• Towards a more flexible and accurate model for grammar levels and associativity

  #71·herbelin opened Jul 22, 2023Member·

  ·
  6

• Short-term roadmap for Coq

  #69·Zimmi48 opened Jul 17, 2023Member·

  ·
  56

• Requirements for supporting Ltac2 debugging with a high-level outline of changes

  #64·jfehrle opened Apr 11, 2022Member·

  ·
  11

• Incremental Include

  #63·gmalecha opened Feb 15, 2022·

  ·
  14

• Separate compilation

  #62·gmalecha opened Feb 14, 2022·

  ·
  34