diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam index d0a66ac2b..cdba4bd54 100644 --- a/coq-mathcomp-analysis.opam +++ b/coq-mathcomp-analysis.opam @@ -27,11 +27,11 @@ depends: [ tags: [ "category:Mathematics/Real Calculus and Topology" "keyword:analysis" - "keyword:extended real number" + "keyword:extended real numbers" "keyword:filter" "keyword:Cantor" "keyword:topology" - "keyword:real number" + "keyword:real numbers" "keyword:sequence" "keyword:convexity" "keyword:Landau notation" diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam index 828c66b68..463a8dfa5 100644 --- a/coq-mathcomp-classical.opam +++ b/coq-mathcomp-classical.opam @@ -30,7 +30,7 @@ tags: [ "category:Mathematics/Classical Logic" "keyword:classical" "keyword:logic" - "keyword:set" + "keyword:sets" "keyword:set theory" "keyword:function" "keyword:cardinal"