diff options
Diffstat (limited to 'doc/refman/Misc.tex')
| -rw-r--r-- | doc/refman/Misc.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Misc.tex b/doc/refman/Misc.tex index 6ce4ee480..e953d2f70 100644 --- a/doc/refman/Misc.tex +++ b/doc/refman/Misc.tex @@ -30,7 +30,7 @@ always transparent. \Example \begin{coq_example*} -Require Coq.Derive.Derive. +Require Coq.derive.Derive. Require Import Coq.Numbers.Natural.Peano.NPeano. Section P. |