Correct and improve implicits and documentation of MatrixGenField

Refactored and completed implicit and scope signatures of constants of
MatrixGenField, the module that contains the construction of an
extension field for an irreducible representation, and for decidability
definitions.
  Completed and corrected some errors in the corresponding header
documentation.

1 files changed, 2 insertions, 0 deletions

diff --git a/ChangeLog b/ChangeLog
index b82a0f4..10e90e9 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -43,6 +43,8 @@
 	  represent the same subspace iff they differ only by a change of
 	  basis.
 
+	* Corrected implicits and documentation of MatrixGenField.
+
 24/04/2018 - compatibility with Coq 8.8 and several small fixes - version 1.7
 
 	* Added compatibility with Coq 8.8 and lost compatibility with