From 2f2b62e202c4585e2b23e1050c7a67f9ef01ad27 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 21 Jun 2014 14:44:25 +0200
Subject: Fixing grammar in doc of Opaque as proposed by Jason (#3389).

---
 doc/refman/RefMan-oth.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/refman/RefMan-oth.tex')

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 20893dc4e1..20ead7cceb 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -1034,8 +1034,8 @@ $\delta$-conversion (unfolding a constant is replacing it by its
 definition).
 
 {\tt Opaque} has also on effect on the conversion algorithm of {\Coq},
-telling to delay the unfolding of a constant as later as possible in
-case {\Coq} has to check the conversion (see Section~\ref{conv-rules})
+telling it to delay the unfolding of a constant as mush as possible when
+{\Coq} has to check the conversion (see Section~\ref{conv-rules})
 of two distinct applied constants.
 
 The scope of {\tt Opaque} is limited to the current section, or
-- 
cgit v1.2.3

