changelog for version 1.0.0 (#1165)

* changelog for version 1.0.0

INSTALL.md

@@ -2,10 +2,10 @@
 
 ## Requirements
 
-- [The Coq Proof Assistant version ≥ 8.15](https://coq.inria.fr)
-- [Mathematical Components version ≥ 1.17.0](https://github.com/math-comp/math-comp)
-- [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap)
-- [Hierarchy builder version >= 1.2.0](https://github.com/math-comp/hierarchy-builder)
+- [The Coq Proof Assistant version ≥ 8.16](https://coq.inria.fr)
+- [Mathematical Components version ≥ 2.0.0](https://github.com/math-comp/math-comp)
+- [Finmap library version ≥ 2.0.0](https://github.com/math-comp/finmap)
+- [Hierarchy builder version >= 1.4.0](https://github.com/math-comp/hierarchy-builder)
 - [bigenough >= 1.0.0](https://github.com/math-comp/bigenough)
 
 These requirements can be installed in a custom way, or through
@@ -48,7 +48,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.7.0
+$ opam install coq-mathcomp-analysis.1.0.0
 ```
 4. Everytime you want to work in this same context, you need to type
 ```
@@ -71,28 +71,28 @@ using [proof general for emacs](https://github.com/ProofGeneral/PG)
 
 ## Break-down of phase 3 of the installation procedure step by step
 
-With the example of Coq 8.15.0 and MathComp 1.17.0. For other versions, update the
+With the example of Coq 8.16.0 and MathComp 2.0.0. For other versions, update the
 version numbers accordingly.
 
-1. Install Coq 8.15.0
+1. Install Coq 8.16.0
 ```
-$ opam install coq.8.15.0
+$ opam install coq.8.16.0
 ```
 2. Install the Mathematical Components
 ```
-$ opam install coq-mathcomp-ssreflect.1.17.0
-$ opam install coq-mathcomp-fingroup.1.17.0
-$ opam install coq-mathcomp-algebra.1.17.0
-$ opam install coq-mathcomp-solvable.1.17.0
-$ opam install coq-mathcomp-field.1.17.0
+$ opam install coq-mathcomp-ssreflect.2.0.0
+$ opam install coq-mathcomp-fingroup.2.0.0
+$ opam install coq-mathcomp-algebra.2.0.0
+$ opam install coq-mathcomp-solvable.2.0.0
+$ opam install coq-mathcomp-field.2.0.0
 ```
 3. Install the Finite maps library
 ```
-$ opam install coq-mathcomp-finmap.1.5.1
+$ opam install coq-mathcomp-finmap.2.0.0
 ```
 4. Install the Hierarchy Builder
 ```
-$ opam install coq-hierarchy-builder.1.2.0
+$ opam install coq-hierarchy-builder.1.6.0
 ```
 5. Download and compile `coq-mathcomp-analysis` without installing
 ```

README.md

@@ -22,6 +22,7 @@ the Coq proof-assistant and using the Mathematical Components library.
 
 - Author(s):
   - Reynald Affeldt (initial)
+  - Alessandro Bruni
   - Yves Bertot
   - Cyril Cohen (initial)
   - Marie Kerjean
@@ -69,7 +70,6 @@ make   # or make -j <number-of-cores-on-your-machine>
 make install
 ```
 
-
 ## Disclaimer
 
 This library is still at an experimental stage.  Contents may
@@ -80,7 +80,7 @@ own risk.
 ## Documentation
 
 Each file is documented in its header
-([coqdoc presentation for the last version](https://math-comp.github.io/analysis/htmldoc_0_7_0/index.html)).
+([coqdoc presentation for the last version](https://math-comp.github.io/analysis/htmldoc_1_0_0/index.html)).
 
 Changes are documented in [CHANGELOG.md](CHANGELOG.md) and
 [CHANGELOG_UNRELEASED.md](CHANGELOG_UNRELEASED.md).

coq-mathcomp-analysis.opam

@@ -51,6 +51,7 @@ tags: [
 ]
 authors: [
   "Reynald Affeldt"
+  "Alessandro Bruni"
   "Yves Bertot"
   "Cyril Cohen"
   "Marie Kerjean"

coq-mathcomp-classical.opam

@@ -38,6 +38,7 @@ tags: [
 ]
 authors: [
   "Reynald Affeldt"
+  "Alessandro Bruni"
   "Yves Bertot"
   "Cyril Cohen"
   "Marie Kerjean"