Merge branch 'master' into wip/binary-readerTwip/binary-readerT

2 files changed, 9 insertions, 9 deletions

diff --git a/docs/opt-coercion/code.sty b/docs/opt-coercion/code.sty
index fe5b38c35c..e5abaaf424 100644
--- a/docs/opt-coercion/code.sty
+++ b/docs/opt-coercion/code.sty
@@ -4,22 +4,22 @@
 % you write "\makeatactive". From then on, inline code is written as @\x
 % -> x_1 & y@. The only difference with what you are used to, is that
 % instead of
-% 
+%
 % @
 %   foo :: Int -> Int
 %   foo = \n -> n+1
 % @
-% 
+%
 % you have to write
-% 
+%
 % \begin{code}
 %   foo :: Int -> Int
 %   foo = \n -> n+1
 % \end{code}
-% 
-% and that you cannot use @ in \section{} and \caption{}. For the paper that occured twice, in which case I had to replace @...@ b y \texttt{...}.
-% 
-% 
+%
+% and that you cannot use @ in \section{} and \caption{}. For the paper that occurred twice, in which case I had to replace @...@ b y \texttt{...}.
+%
+%
 % code.sty  --- nice verbatim mode for code
 
 % To get '@' use \verb+@+
diff --git a/docs/opt-coercion/fc-normalization-rta.tex b/docs/opt-coercion/fc-normalization-rta.tex
index a1e7d4201d..0600427e98 100755
--- a/docs/opt-coercion/fc-normalization-rta.tex
+++ b/docs/opt-coercion/fc-normalization-rta.tex
@@ -227,7 +227,7 @@ which has evolved from System F to System FC
 source-language features of
 \emph{GADTs}~\cite{cheney-hinze:phantom-types,sheard:omega,spj+:gadt}
 and \emph{type families}~\cite{Kiselyov09funwith,chak+:synonyms}.
-The key feature that allows System FC to accomodate GADTs and type
+The key feature that allows System FC to accommodate GADTs and type
 families is its use of explicit \emph{coercions} that witness the
 equality of two syntactically-different types.  Coercions are erased
 before runtime but, like types, serve as a static consistency
@@ -802,7 +802,7 @@ $$
 \gamma ; \sym{\gamma} & \rsa{} & \refl{\tau} & \text{if}\,\gamma : \tau \psim \phi 
 \end{array}
 $$
-But ther are much more complicated rewrites to consider.
+But there are much more complicated rewrites to consider.
 Consider these coercions, where $C_N$ is the axiom generated by the newtype coercion in 
 Section~\ref{sec:newtype}:
 $$