diff options
| author | letouzey | 2017-07-27 17:09:21 +0200 |
|---|---|---|
| committer | GitHub | 2017-07-27 17:09:21 +0200 |
| commit | d09c02c2e35e7dd076a3ae95e7ed7ac444a976a3 (patch) | |
| tree | 6d73a2668e0ea9e24b3c331b5cc513833805d129 | |
| parent | ce3ed09acebe048f1a361ed6440a520b166a13b8 (diff) | |
Extraction.tex: mention the possible "From Coq Require Extraction"
| -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}. |