From 4b4fc278887d33299aea32aceea93e9849a65855 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 30 Mar 2016 17:34:44 +0200
Subject: TYPOGRAPHY: adding missing \noindent macros

---
 doc/refman/RefMan-cic.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 1554ee04d3..50f4dc1330 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 :=
-- 
cgit v1.2.3