From 2268a3e7e84735c072bd2d9d25e6cc16b2a29281 Mon Sep 17 00:00:00 2001
From: William Lawvere <mundungus.corleone@gmail.com>
Date: Fri, 7 Jul 2017 19:26:19 -0700
Subject: RefMan-ext: fix some typos

---
 doc/refman/RefMan-ext.tex | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index f338c3055..3bc5169c5 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -705,18 +705,18 @@ when the {\tt FunInd} library has been loaded via {\tt Require Import FunInd}:
 This command can be seen as a generalization of {\tt Fixpoint}.  It is actually
 a wrapper for several ways of defining a function \emph{and other useful
   related objects}, namely: an induction principle that reflects the
-recursive structure of the function (see \ref{FunInduction}), and its
+recursive structure of the function (see \ref{FunInduction}) and its
 fixpoint equality.
  The meaning of this
 declaration is to define a function {\it ident}, similarly to {\tt
   Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be
-given (unless the function is not recursive), but it must not
-necessary be \emph{structurally} decreasing. The point of the {\tt
+given (unless the function is not recursive), but it might not
+necessarily be \emph{structurally} decreasing. The point of the {\tt
   \{\}} annotation is to name the decreasing argument \emph{and} to
 describe which kind of decreasing criteria must be used to ensure
 termination of recursive calls.
 
-The {\tt Function} construction enjoys also the {\tt with} extension
+The {\tt Function} construction also enjoys the {\tt with} extension
 to define mutually recursive definitions. However, this feature does
 not work for non structural recursive functions. % VRAI??
 
@@ -749,7 +749,7 @@ Function plus (n m : nat) {struct n} : nat :=
 \end{coq_example*}
 
 \paragraph[Limitations]{Limitations\label{sec:Function-limitations}}
-\term$_0$ must be build as a \emph{pure pattern-matching tree}
+\term$_0$ must be built as a \emph{pure pattern-matching tree}
 (\texttt{match...with}) with applications only \emph{at the end} of
 each branch.  
 
@@ -776,7 +776,7 @@ For now dependent cases are not treated for non structurally terminating functio
 
   The generation of the graph relation \texttt{(R\_\ident)} used to
   compute the induction scheme of \ident\ raised a typing error. Only
-  the ident is defined, the induction scheme will not be generated.
+  the ident is defined; the induction scheme will not be generated.
 
   This error happens generally when:
 
@@ -848,14 +848,14 @@ the following:
       being the decreasing argument and \term$_1$ being a function
       from type of \ident$_0$ to \texttt{nat} for which value on the
       decreasing argument decreases (for the {\tt lt} order on {\tt
-      nat}) at each recursive call of \term$_0$, parameters of the
+      nat}) at each recursive call of \term$_0$. Parameters of the
       function are bound in  \term$_0$;
 \item {\tt \{wf} \term$_1$ \ident$_0${\tt\}} with \ident$_0$ being
       the decreasing argument and \term$_1$ an ordering relation on
       the type of \ident$_0$ (i.e. of type T$_{\ident_0}$
       $\to$ T$_{\ident_0}$ $\to$ {\tt Prop}) for which
       the decreasing argument decreases at each recursive call of
-      \term$_0$. The order must be well founded. parameters of the
+      \term$_0$. The order must be well founded. Parameters of the
       function are bound in  \term$_0$.
 \end{itemize} 
 
-- 
cgit v1.2.3


From 8f2c2a758f3d5e01238760be12c83d4ff08d5276 Mon Sep 17 00:00:00 2001
From: william-lawvere <mundungus.corleone@gmail.com>
Date: Fri, 14 Jul 2017 17:13:54 -0700
Subject: Update with non structurally recursive

---
 doc/refman/RefMan-ext.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 3bc5169c5..713f344cb 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -718,7 +718,7 @@ termination of recursive calls.
 
 The {\tt Function} construction also enjoys the {\tt with} extension
 to define mutually recursive definitions. However, this feature does
-not work for non structural recursive functions. % VRAI??
+not work for non structurally recursive functions. % VRAI??
 
 See the documentation of {\tt functional induction}
 (see Section~\ref{FunInduction}) and {\tt Functional Scheme}
-- 
cgit v1.2.3