From 961b5160dc4872c60a9adfa7abe9efd5cb140690 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 17 Dec 2011 22:59:29 +0000
Subject: 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
---
 doc/refman/RefMan-ext.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/refman')

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}{}
-- 
cgit v1.2.3