From 8f96f8194608c99ad8efa201c24b527dbc530537 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 29 Oct 2015 12:08:49 +0100
Subject: CLEANUP PROPOSITION: The removed paragraph is not essential for this
 chapter. That kind of information is more appropriate for Section 1.2.

---
 doc/refman/RefMan-cic.tex | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index b1becba3f5..ed7889e480 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -178,15 +178,6 @@ More precisely the language of the {\em Calculus of Inductive
 %\item cofixpoint ...
 \end{enumerate}
 
-\paragraph{Notations.} Application associates to the left such that
-$(t\;t_1\;t_2\ldots t_n)$ represents $(\ldots ((t\;t_1)\;t_2)\ldots t_n)$. The
-products and arrows associate to the right such that $\forall~x:A,B\ra C\ra
-D$ represents $\forall~x:A,(B\ra (C\ra D))$.  One uses sometimes
-$\forall~x~y:A,B$ or
-$\lb x~y:A\mto t$ to denote the abstraction or product of several variables
-of the same type. The equivalent formulation is $\forall~x:A, \forall y:A,B$ or
-$\lb x:A \mto \lb y:A \mto t$
-
 \paragraph{Free variables.}
 The notion of free variables is defined as usual.  In the expressions
 $\lb x:T\mto U$ and $\forall x:T, U$ the occurrences of $x$ in $U$
-- 
cgit v1.2.3