diff options
| -rw-r--r-- | doc/refman/Extraction.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 8271c7c324..9e74463e18 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -284,7 +284,7 @@ Extract Inductive prod => "(*)" [ "(,)" ]. \asubsection{Avoiding conflicts with existing filenames} -\comindex{Extraction Blaclist} +\comindex{Extraction Blacklist} When using {\tt Extraction Library}, the names of the extracted files directly depends from the names of the \Coq\ files. It may happen that |