Fixed some typos.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9789 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 2 insertions, 2 deletions

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
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 2403c07a6d..d4f76075ce 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1233,7 +1233,7 @@ scheme of name {\qualid}. It does not expect that the type of
   where {\qualid} is an induction principle with complex predicates
   (like the ones generated by function induction).
 
-\item {\tt induction {\term} using {\qualid} as {\intropattern}}
+\item {\tt induction {\term} as {\intropattern} using {\qualid}}
 
   This combines {\tt induction {\term} using {\qualid}}
 and {\tt induction {\term} as {\intropattern}}.