All notable changes to this project will be documented in this file.
The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.
0.2.1 - 2024-12-02
- Use new display type for
orderType
, as in MathComp 2.3.0. The generated instances now use the default display.
- Simplify the type of derived isFinite instances to avoid a non-forgetful inheritance warning.
0.2.0 - 2023-09-22
-
Make Deriving compatible with Hierarchy Builder and MathComp 2.0.0.
-
Following the changes of terminology in MathComp, the syntax for deriving the base mixins has now the form
[derive [<flag>] <mixin> for <type>]
, where<flag>
is one ofred
,nored
orlazy
.<mixin>
is one ofhasDecEq
,hasChoice
,isCountable
,isFinite
orisOrder
.
- The derivation forms
[derive ...]
that mention the old MathComp mixin nameseqMixin
,choiceMixin
,countMixin
,finMixin
andorderMixin
are deprecated. Use the new names for those mixins, as explained in the previous section.
0.1.1 - 2023-03-10
- Add
global
locality annotations to comply with newer versions of Coq
0.1.0 - 2020-02-24
- First version supporting inductive types.