From d09c02c2e35e7dd076a3ae95e7ed7ac444a976a3 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 27 Jul 2017 17:09:21 +0200
Subject: Extraction.tex: mention the possible "From Coq Require Extraction"

---
 doc/refman/Extraction.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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}.
 
-- 
cgit v1.2.3