From bccc54dc85e2d9cd7248c24a576d6092630fb51d Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Sat, 28 Jul 2018 21:30:02 +0200
Subject: moving countalg and closed_field around

- countalg goes to the algebra package
- finalg now get the expected inheritance from countalg
- closed_field now contains the construction of algebraic closure for countable fields (previously in countalg)
- proof of quantifier elimination for closed field rewritten in a monadic style
---
 ChangeLog | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'ChangeLog')

diff --git a/ChangeLog b/ChangeLog
index 2e8a495..c651b13 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -3,6 +3,15 @@
 	* Added companion matrix of a polynomial `companionmx p` and the
 	  theorems: companionmxK, map_mx_companion and companion_map_poly
 
+	* Reshuffled theorems inside files and packages:
+	  * countalg goes from the field to the algebra package
+	  * finalg now gets inheritance from countalg
+	  * closed_field now contains the construction of algebraic closure
+	    for countable fields that used to be in countalg.
+
+        * Rewritten proof of quantifier elimination for closed field in a
+	  monadic style.
+
 	* Added allsigs, the dependent version of allpairs,
 	  with notation `[seq E | i <- s & j <- t]`
 
-- 
cgit v1.2.3