There are several libraries that build on top of the base
Mathematical Components libraries, e.g.:
@@ -368,7 +368,7 @@
Install Other Mathematical Components Libraries
A layer for classical reasoning (developed along MathComp Analysis)
-- Available as the opam package
coq-mathcomp-classic
+- Available as the opam package
coq-mathcomp-classical
MathComp Analysis
diff --git a/installation.org b/installation.org
index 462773b8..c9c2d4ec 100644
--- a/installation.org
+++ b/installation.org
@@ -80,7 +80,7 @@ Extensions:
3. [[https://github.com/math-comp/real-closed][Theorems for Real Closed Fields]]
- Available as the opam package ~coq-mathcomp-real-closed~
4. A layer for classical reasoning (developed along [[https://github.com/math-comp/analysis][MathComp Analysis]])
- - Available as the opam package ~coq-mathcomp-classic~
+ - Available as the opam package ~coq-mathcomp-classical~
4. [[https://github.com/math-comp/analysis][MathComp Analysis]]
- Available as the opam package ~coq-mathcomp-analysis~