Command Arguments: standardizing format of error messages and American spelling.

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

1 files changed, 2 insertions, 2 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 47a2e462dd..472d7903b8 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1148,7 +1148,7 @@ In case one wants that some arguments of a given object (constant,
 inductive types, constructors, assumptions, local or not) are always
 inferred by Coq, one may declare once and for all which are the expected
 implicit arguments of this object. There are two ways to do this,
-a-priori and a-posteriori. 
+a priori and a posteriori.
 
 \subsubsection{Implicit Argument Binders}
 
@@ -1190,7 +1190,7 @@ usual implicit arguments disambiguation syntax.
 
 \subsubsection{Declaring Implicit Arguments}
 
-To set implicit arguments for a constant a-posteriori, one can use the
+To set implicit arguments for a constant a posteriori, one can use the
 command:
 \begin{quote}
 \tt Arguments {\qualid} \nelist{\possiblybracketedident}{}