diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 4 |
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}{} |