From 4adb34c2ea8a602f36230b6b10cfeacc3f6be3f4 Mon Sep 17 00:00:00 2001
From: glondu
Date: Wed, 18 Apr 2007 18:18:58 +0000
Subject: Fixed some typos.

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

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

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 5a648ae6a0..769927cafa 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1010,7 +1010,7 @@ the third argument has type {\tt True}, then any {\tt P} of the form
 be a solution of the inference problem.
 
 \paragraph{Contextual Implicit Arguments.} 
-An implicit argument can be {\em contextual} or non. An implicit
+An implicit argument can be {\em contextual} or not. An implicit
 argument is said {\em contextual} if it can be inferred only from the
 knowledge of the type of the context of the current expression. For
 instance, the only argument of
-- 
cgit v1.2.3