From 718ae58fbf794dd069d0d4a5e35da697f0aabba9 Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Fri, 14 Dec 2018 17:41:37 +0100
Subject: 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.
---
 ChangeLog | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'ChangeLog')

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
-- 
cgit v1.2.3