Merge pull request #262 from math-comp/cancel-lemmas-implicit

Cancel lemmas implicit

1 files changed, 14 insertions, 1 deletions

diff --git a/ChangeLog b/ChangeLog
index 4f17072..b82a0f4 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -24,7 +24,20 @@
 	  from eqtype.v. They were already in ssrfun.v.
 
 	* Specialized `bool_irrelevance` so that the statement reflects
-	  the name
+	  the name.
+
+	* Changed the shape of the type of FieldMixin to allow one-line
+	  in-proof definition of bespoke fieldType structure.
+
+	* Refactored and extended Arguments directives to provide more
+	  comprehensive signature information.
+
+	* Added maximal implicits to reflection, injectivity and cancellation
+	  lemmas so that they are easier to pass to combinator lemmas such as
+	  sameP, inj_eq or canLR.
+
+	* Added reindex_inj s shorthand for reindexing a bigop with a
+	  permutation s.
 
 	* Added lemma `eqmxMunitP`: two matrices with the same shape
 	  represent the same subspace iff they differ only by a change of