diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam index f2228ea78..d0a66ac2b 100644 --- a/coq-mathcomp-analysis.opam +++ b/coq-mathcomp-analysis.opam @@ -27,13 +27,26 @@ depends: [ tags: [ "category:Mathematics/Real Calculus and Topology" "keyword:analysis" + "keyword:extended real number" + "keyword:filter" + "keyword:Cantor" "keyword:topology" - "keyword:real numbers" + "keyword:real number" + "keyword:sequence" + "keyword:convexity" + "keyword:Landau notation" + "keyword:logarithm" + "keyword:sin" + "keyword:cos" + "keyword:tangent" + "keyword:trigonometric function" + "keyword:exponential" "keyword:differentiation" "keyword:derivative" "keyword:measure theory" "keyword:integration" "keyword:Lebesgue" + "keyword:probability" "logpath:mathcomp.analysis" ] authors: [ diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam index 463a8dfa5..828c66b68 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:sets" + "keyword:set" "keyword:set theory" "keyword:function" "keyword:cardinal"