changelog

Changelog.md

@@ -4,10 +4,14 @@
 
 ### General
 
-- **Change** For a structure S on a subject of type T, declares sort as an
-	Elpi coercion from S to T and an Epli coercion from T to S whenever T
-	has no gref.
-- **Change** Declares axioms_ as a typeclass
+- **Change** For a structure `S` on a subject of type `T`, declares `S.sort` as
+	an Elpi coercion from `S.type` to `T` and `S.pack` as an Epli coercion from
+	`T` to `S.type` whenever `T` is not a global type (e.g. a variable). Note
+	that `S.pack` can cast a `t : T` to `S.type` only if an instance of the
+	class `S` on `t` is found by type class inference
+- **Change** `HB.structure` declares the class of a structure (`axioms_`) as a
+	type class on the subject with all arguments in output mode but for the
+	subject that is in input mode.
 
 ## [1.7.0] - 2024-01-10