diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-31 14:28:28 +0200 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-01 19:18:58 +0200 |
commit | a7a3f6510643b4fa4bc3299c5111c44b4887873d (patch) | |
tree | db2f92c2dcd38001c32959ebecfbd74b17b58315 /doc | |
parent | 19394cc1e21c775e2151eea07970a98e6ddbce6a (diff) |
Fix English spelling -> American spelling in doc.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-ltac.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index d713661c2..75aa33d7a 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -732,7 +732,7 @@ As a workaround, one could use the following variant of {\tt context}: {\tt appcontext} {\ident} {\tt [} {\cpattern} {\tt ]} \end{quote} This syntax is now deprecated, as {\tt context} behaves as intended. The former -behaviour can be retrieved with the {\tt Tactic Compat Context} flag. +behavior can be retrieved with the {\tt Tactic Compat Context} flag. \end{Variants} @@ -879,7 +879,7 @@ The following returns the type of {\term}: The terms built in Ltac are well-typed by default. It may not be appropriate for building large terms using a recursive Ltac function: the term has to be entirely type checked at each step, resulting in -potentially very slow behaviour. It is possible to build untyped terms using Ltac with the syntax +potentially very slow behavior. It is possible to build untyped terms using Ltac with the syntax \begin{quote} {\tt uconstr :} {\term} |