diff options
Diffstat (limited to 'doc/refman/Extraction.tex')
| -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 5d7ec66fa3..8cb049d50e 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -22,7 +22,7 @@ be used (abusively) to refer to any of the three. Before using any of the commands or options described in this chapter, the extraction framework should first be loaded explicitly via {\tt Require Extraction}, or via the more robust -{\tt Require Coq.extraction.Extraction}. +{\tt From Coq Require Extraction}. Note that in earlier versions of Coq, these commands and options were directly available without any preliminary {\tt Require}. |