Merge pull request #301 from math-comp/update-changelog

Update Changelog.md

Changelog.md

@@ -1,5 +1,16 @@
 # Changelog
 
+## [1.3.0] - 2022-07-27
+
+Compatible with
+- Coq 8.15 with Coq-Elpi 1.14.x
+- Coq 8.16 with Coq-Elpi 1.15.x
+
+### General
+
+- **Fix** Structures can be keyd on sorts (eg `Prop`) and products (eg `T -> U`)
+- **New** Mixin parameters can depend on structure instances inferred using previous mixins (see [this test](tests/interleave_context.v))
+
 ## [1.2.1] - 2022-01-10
 
 Compatible with

tests/interleave_context.v

@@ -7,9 +7,12 @@ HB.structure Definition A n := { T of HasA n T }.
 HB.mixin Record HasB (X : A.type 0) (T : Type) := { b : X -> T }.
 HB.structure Definition B (X : A.type 0) := { T of HasB X T }.
 
-#[verbose]
+(* Since `B` expects an argument of type `A.type 0` (and not just
+   just the naked type `T`) we pass `A.clone 0 T _`
+   (of type `A.type 0`) and inference uses the first
+   parameter `A` to elaborate it. *)
 HB.mixin Record IsSelfA T of A 0 T & B (A.clone 0 T _) T := {}.
-#[verbose]
+
 HB.structure Definition SelfA := { T of IsSelfA T }.
 
 HB.factory Record IsSelfA' T := { a : T ; b : T -> T}.
@@ -19,5 +22,4 @@ HB.builders Context T of IsSelfA' T.
   HB.instance Definition _ := IsSelfA.Build T.
 HB.end.
 
-#[verbose]
-  HB.instance Definition _ := IsSelfA'.Build nat 0 id.
+HB.instance Definition _ := IsSelfA'.Build nat 0 id.