From 47f4578c9a1ef1b37cba1bd15fc914bca2bd95dd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 14 Sep 2001 15:44:34 +0000
Subject: Orthographe

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

diff --git a/doc/Changes.tex b/doc/Changes.tex
index bf27424665..7b10f4f825 100755
--- a/doc/Changes.tex
+++ b/doc/Changes.tex
@@ -12,6 +12,7 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \shorttitle{Changes from {\Coq} V6.3.1 to {\Coq} V7}
 
+
 %This document describes the main differences between {\Coq} V6.3.1 and
 %V7. This new version of {\Coq} is characterized by fixed bugs, and
 %improvement of implicit arguments synthesis and speed in tactic
@@ -335,10 +336,10 @@ can be visited at the following URL:\\
 
 {\sf http://logical.inria.fr/\~{}delahaye/}
 
-\paragraph{Tactic debuger}
+\paragraph{Tactic debugger}
 
   \paragraph{{\tt Debug $($ On $|$ Off $)$}} turns on/off the tactic
-  debuger for $\ltac$.
+  debugger for $\ltac$.
   This is still very experimental and no documentation is provided yet.
 
 
@@ -511,6 +512,7 @@ Print exists.
 Implicits exists [1].
 Print exists.
 \end{coq_example}
+
 \subsection{Syntax standardisation}
 
 The commands on the left are now equivalent to (old) commands on
-- 
cgit v1.2.3