diff --git a/doc/languages-frameworks/coq.xml b/doc/languages-frameworks/coq.xml
index d16c9f3dc87..43da6a3f49d 100644
--- a/doc/languages-frameworks/coq.xml
+++ b/doc/languages-frameworks/coq.xml
@@ -11,31 +11,53 @@
     in the Coq derivation.
   </para>
   <para>
-    Some libraries require OCaml and sometimes also Camlp5. The exact
-    versions that were used to build Coq are saved in the
+    Some libraries require OCaml and sometimes also Camlp5 or findlib.
+    The exact versions that were used to build Coq are saved in the
     <literal>coq.ocaml</literal> and <literal>coq.camlp5</literal>
-    attributes.
+    and <literal>coq.findlib</literal> attributes.
+  </para>
+  <para>
+    Coq libraries may be compatible with some specific versions of Coq only.
+    The <liberal>compatibleCoqVersions</liberal> attribute is used to
+    precisely select those versions of Coq that are compatible with this
+    derivation.
   </para>
   <para>
     Here is a simple package example. It is a pure Coq library, thus it
-    only depends on Coq. Its <literal>makefile</literal> has been
-    generated using <literal>coq_makefile</literal> so we only have to
+    depends on Coq. It builds on the Mathematical Components library, thus it
+    also takes <literal>mathcomp</literal> as <literal>buildInputs</literal>.
+    Its <literal>Makefile</literal> has been generated using
+    <literal>coq_makefile</literal> so we only have to
     set the <literal>$COQLIB</literal> variable at install time.
   </para>
   <programlisting>
-{stdenv, fetchurl, coq}:
-stdenv.mkDerivation {
-  src = fetchurl {
-    url = http://coq.inria.fr/pylons/contribs/files/Karatsuba/v8.4/Karatsuba.tar.gz;
-    sha256 = "0ymfpv4v49k4fm63nq6gcl1hbnnxrvjjp7yzc4973n49b853c5b1";
+{ stdenv, fetchFromGitHub, coq, mathcomp }:
+
+stdenv.mkDerivation rec {
+  name = "coq${coq.coq-version}-multinomials-${version}";
+  version = "1.0";
+  src = fetchFromGitHub {
+    owner = "math-comp";
+    repo = "multinomials";
+    rev = version;
+    sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
   };
 
-  name = "coq-karatsuba";
-
   buildInputs = [ coq ];
+  propagatedBuildInputs = [ mathcomp ];
 
   installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+
+  meta = {
+    description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
+    inherit (src.meta) homepage;
+    license = stdenv.lib.licenses.cecill-b;
+    inherit (coq.meta) platforms;
+  };
+
+  passthru = {
+    compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ];
+  };
 }
 </programlisting>
 </section>
-