modified miscellaneous-extensions.rst

To fix doc
Villetaneuse · Nov 11, 2023 · 9fa5ea9 · 9fa5ea9
1 parent 345be7f
commit 9fa5ea9
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.