Regular Language Representations in Coq 1.2.2

This release is known to support MathComp version 2.0.0 to 2.4.0 and Coq 8.16 to 9.0.

Changes:

• Support for MathComp 2.4.0

Regular Language Representations in Coq 1.2.1

This release is known to support MathComp version 2.0.0 to 2.2.0 and Coq 8.16 to 8.19.

Changes:

• Support for MathComp 2.2.0

Regular Language Representations in Coq 1.2.0

This release supports MathComp version 2.0.0 and Coq 8.16 to 8.18.

Changes:

• Port to MathComp 2 and Hierarchy Builder by Pierre Roux, dropping support for earlier MathComp versions.
• Remove some utility lemmas that now exist upstream.

Regular Language Representations in Coq 1.1.3

This is a maintenance release and supports MathComp versions 1.11.0 to 1.14.0 in combination with compatible versions of Coq, at least 8.12 to 8.15.

Changes:

• Removed various lemmas from misc.v that now have replacements in MathComp.
• Moved a few lemmas from coq-community/regexp-Brzozowski to this development.

Regular Language Representations in Coq 1.1.2

This is a maintenance release and has been tested with

• coq 8.13 + mathcomp-1.12
• coq 8.12 + mathcomp-1.12
• coq 8.12 + mathcomp-1.11
• coq 8.11 + mathcomp-1.10
• coq 8.10 + mathcomp-1.9

Changes:

• explicit hint locality to avoid warnings in coq-8.13
• uses omega have been replaced lia

Regular Language Representations in Coq 1.1.1

This is a maintenance release and has been tested with:

• coq 8.12 + mathcomp-1.11.0
• coq 8.11 + mathcomp-1.10.0
• coq 8.10 + mathcomp-1.9.0

Changes:

• use of Proof using to enable parallel builds for sections (#17).

Regular Language Representations in Coq 1.1

Compatibility release for coq-8.10 / mathcomp-1.9