From a7a3f6510643b4fa4bc3299c5111c44b4887873d Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 31 Jul 2014 14:28:28 +0200 Subject: Fix English spelling -> American spelling in doc. --- doc/refman/RefMan-ltac.tex | 4 ++-- 1 file 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} -- cgit v1.2.3