From f52d396b1c1499cb12531d89e77341326192b53d Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 12 Nov 2003 16:46:06 +0000
Subject: En fait les Import des Require sont de nouveau utiles

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8353 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Extraction.tex | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index 0ad4410b19..629b84530b 100755
--- a/doc/Extraction.tex
+++ b/doc/Extraction.tex
@@ -369,7 +369,7 @@ We can now extract this program to \ocaml:
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
-Require Euclid.
+Require Import Euclid.
 Extraction Inline Wf_nat.gt_wf_rec Wf_nat.lt_wf_rec.
 Recursive Extraction  eucl_dev.
 \end{coq_example}
@@ -421,13 +421,13 @@ treesort}, whose type is shown below:
 
 \begin{coq_eval}
 Reset Initial.
-Require Relation_Definitions.
-Require List.
-Require Sorting.
-Require Permutation.
+Require Import Relation_Definitions.
+Require Import List.
+Require Import Sorting.
+Require Import Permutation.
 \end{coq_eval}
 \begin{coq_example}
-Require Heap.
+Require Import Heap.
 Check treesort.
 \end{coq_example}
 
-- 
cgit v1.2.3