diff options
-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} |