From a4e7def8e02b03fdcd8a5eab062e14313bff5104 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 18 Jan 2002 08:31:12 +0000
Subject: typo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8271 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Extraction.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index 1668e8e968..1477503409 100755
--- a/doc/Extraction.tex
+++ b/doc/Extraction.tex
@@ -321,7 +321,7 @@ Extract Inductive sumbool => bool [ true false ].
  the future. In the meanwhile you can have a look at the \Coq\
  contributions. Several of them use extraction to produce certified 
  programs. In particular the following ones have an automatic extraction
- test (just run make in those directory): 
+ test (just run \verb|make| in those directories): 
 
  \begin{itemize}
  \item Bordeaux/Additions
-- 
cgit v1.2.3