Enriched numClosedFieldType so that it factors a lot of theory from both complex and algC.

The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory
have been moved to the numClosedFieldType structure in ssrnum.
This covers boths the uses in algC and complex.v. To that end the
numClosedFieldType structure has been enriched with conjugation and 'i.
Note that 'i can be deduced from the property of algebraic closure and is
only here to let the user chose which definitional equality should hold
on 'i. Same thing for conjC that could be written  `|x|^+2/x, the only
nontrivial (up to my knowledge) property is the fact that conjugation
is a ring morphism.

1 files changed, 13 insertions, 0 deletions

diff --git a/etc/ChangeLog b/etc/ChangeLog
index ee28d7d..e33edb4 100644
--- a/etc/ChangeLog
+++ b/etc/ChangeLog
@@ -1,3 +1,16 @@
+25/08/2016 - refactoring of algC and complex in ssrnum  - development version
+	* ssrnum's interface numClosedFieldType factors some theory from
+	  both complex and algC. Because of that Re, Im, 'i, conjC, n.-root
+	  and sqrtC are not specialized to algC anymore. In case of
+	  ambiguity, they should be instanciated with algC using typing
+	  constraints. Moreoever some lemmas from the theory like conjCK
+	  have an extra nonmaximal implicit argument (C :
+	  numClosedFieldType) which could break some proofs. Additionally,
+	  ad-hoc constructions from complex.v like -*+ or complex.Re are now
+	  deprecated and one should rely solely on the ssrnum interface. The
+	  next revision might definietly hide those constructions under a
+	  module.
+
 24/11/2015 - major reorganization of the archive - version 1.6
 	* Files split into subdirectories: ssreflect, algebra, fingroup,
 	  solvable, field and character. In this way the user can decide