diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-03-30 17:34:44 +0200 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-04-12 11:17:43 +0200 |
| commit | 4b4fc278887d33299aea32aceea93e9849a65855 (patch) | |
| tree | bc90eb2ce7489dc5673087f48701306639326ff7 | |
| parent | d5cbd7b881dcc8b3599b3330e342f0aa55ef467f (diff) | |
TYPOGRAPHY: adding missing \noindent macros
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 1554ee04d..50f4dc133 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -552,14 +552,14 @@ The declaration for parameterized lists is: \end{array}\right]} \vskip.5em -which corresponds to the result of the \Coq\ declaration: +\noindent which corresponds to the result of the \Coq\ declaration: \begin{coq_example*} Inductive list (A:Set) : Set := | nil : list A | cons : A -> list A -> list A. \end{coq_example*} -The declaration for a mutual inductive definition of forests and trees is: +\noindent The declaration for a mutual inductive definition of forests and trees is: \vskip.5em \ind{}{\left[\begin{array}{r \colon l}\tree&\Set\\\forest&\Set\end{array}\right]} {\left[\begin{array}{r \colon l} @@ -569,7 +569,7 @@ The declaration for a mutual inductive definition of forests and trees is: \end{array}\right]} \vskip.5em -which corresponds to the result of the \Coq\ +\noindent which corresponds to the result of the \Coq\ declaration: \begin{coq_example*} Inductive tree : Set := @@ -579,7 +579,7 @@ with forest : Set := | consf : tree -> forest -> forest. \end{coq_example*} -The declaration for a mutual inductive definition of even and odd is: +\noindent The declaration for a mutual inductive definition of even and odd is: \newcommand\GammaI{\left[\begin{array}{r \colon l} \even & \nat\ra\Prop \\ \odd & \nat\ra\Prop @@ -594,7 +594,7 @@ The declaration for a mutual inductive definition of even and odd is: \vskip.5em \ind{1}{\GammaI}{\GammaC} \vskip.5em -which corresponds to the result of the \Coq\ +\noindent which corresponds to the result of the \Coq\ declaration: \begin{coq_example*} Inductive even : nat -> Prop := |