diff --git a/opam b/opam index d6c8f63..c313d81 100644 --- a/opam +++ b/opam @@ -15,8 +15,12 @@ depends: [ "coq-mathcomp-ssreflect" { (>= "1.8.0" & < "1.9.0~") | (= "dev")} "coq-mathcomp-bigenough" { (>= "1.0.0" & < "1.1.0~") } ] - -tags: [ "keyword:finmap" "keyword:finset" "keyword:multiset"] +tags: [ "keyword:finmap" "keyword:finset" "keyword:multiset" "keyword:order"] authors: [ "Cyril Cohen " ] - -synopsis: "A finset and finmap library" +synopsis: "Finite sets, finite maps, finitely supported functions, orders" +description: """ +This library is an extension of mathematical component in order to +support finite sets and finite maps on choicetypes (rather that finite +types). This includes support for functions with finite support and +multisets. The library also contains a generic order and set libary, +which will be used to subsume notations for finite sets, eventually."""