diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam index f2228ea78..cdba4bd54 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 numbers" + "keyword:filter" + "keyword:Cantor" "keyword:topology" "keyword:real numbers" + "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: [