Buchberger 8.18 maintenance release

Maintenance release compatible with Coq 8.17, 8.18, and 8.19 with the following changes:

Fixed

• Compatibility with Coq 8.19 and later

Buchberger 8.17 maintenance release

Maintenance release compatible with Coq 8.17 and 8.18, with the following changes:

Changed

• Restrict to Coq 8.17 and later

Fixed

• Deprecation warnings for lists in Coq 8.18

Buchberger 8.16 maintenance release

Maintenance release compatible with Coq 8.16, with the following changes:

Changed

• Use axiom-free lexical product from Stdlib
• Restrict to Coq 8.16 and later

Fixed

• Deprecation warnings for Nat module in Coq 8.16

Buchberger 8.14 maintenance release

Maintenance release compatible with Coq 8.12 to 8.15, featuring the following changes:

Added

• Link to Persson and Coquand's TYPES 1998 paper on Gröbner bases in type theory

Changed

• Change proofs to avoid depending on UIP, i.e., axiom Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq (@SkySkimmer)

Buchberger 8.13 maintenance release

Maintenance release with Coq 8.12 and 8.13 support, featuring the following changes:

Added

• Proof using annotations

Fixed

• Add hint locality

Changed

• Non-Prop definitions are transparent
• Avoid global hint locality

Buchberger 8.11 maintenance release

Maintenance release with Coq 8.11 compatibility, featuring the following changes:

Added

• Support for building with dune, including extraction of OCaml code
• Metadata on project, including detailed publication information

Fixed

• Compatibility with Coq 8.11

Changed

• Reorganize files into subdirectories
• Generalize definitions and results from Set to Type