From 0ad9953cfacda53dea9b08f3b5b60ee5531b0850 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 5 Nov 2015 15:42:17 +0100
Subject: CLEANUP: removing duplicate paragraph

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

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index f69b402783..bea0079a5c 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1272,12 +1272,6 @@ in~\cite{Coq92}.  One is the definition by pattern-matching. The second one is a
 \subsubsection[The {\tt match\ldots with \ldots end} construction.]{The {\tt match\ldots with \ldots end} construction.\label{Caseexpr}
 \index{match@{\tt match\ldots with\ldots end}}}
 
-The basic idea of this operator is that we have an object
-$m$ in an inductive type $I$ and we want to prove a property
-which possibly depends on $m$. For this, it is enough to prove the
-property for $m = (c_i~u_1\ldots  u_{p_i})$ for each constructor of $I$.
-
-
 The basic idea of this operator is that we have an object
 $m$ in an inductive type $I$ and we want to prove a property
 which possibly depends on $m$. For this, it is enough to prove the
-- 
cgit v1.2.3