modified miscellaneous-extensions.rst

To fix doc
Villetaneuse · Oct 15, 2023 · 11ab515 · 11ab515
1 parent 697b152
commit 11ab515
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -29,7 +29,7 @@ it provides the following command:
   .. coqtop:: all
 
      Require Coq.derive.Derive.
-     Require Import Coq.Numbers.Natural.Peano.NPeano.
+     Require Import PeanoNat.
 
      Section P.