From df7ee5401f9010ca659da7bdb11cf85f3c79021b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 5 Jan 2004 19:11:26 +0000
Subject: MAJ pour compilation coq-tex correcte

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

(limited to 'doc/RefMan-ltac.tex')

diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
index 06307a0304..eced8099aa 100644
--- a/doc/RefMan-ltac.tex
+++ b/doc/RefMan-ltac.tex
@@ -683,6 +683,7 @@ possible with the syntax:
 \begin{center}
 \fbox{\begin{minipage}{0.95\textwidth}
 \begin{coq_example*}
+Require Import List.
 Section Sort.
 Variable A : Set.
 Inductive permut : list A -> list A -> Prop :=
-- 
cgit v1.2.3