Typo in documentation of Derive

1 files changed, 1 insertions, 1 deletions

diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
index 80ea8a1166..b6c35d8fa7 100644
--- a/doc/sphinx/addendum/miscellaneous-extensions.rst
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -11,7 +11,7 @@ Program derivation
 |Coq| comes with an extension called ``Derive``, which supports program
 derivation. Typically in the style of Bird and Meertens or derivations
 of program refinements. To use the Derive extension it must first be
-required with ``Require Coq.Derive.Derive``. When the extension is loaded,
+required with ``Require Coq.derive.Derive``. When the extension is loaded,
 it provides the following command:
 
 .. cmd:: Derive @ident SuchThat @term As @ident