From 47c235b94e8870043deb04b65aad08eac8f7ae3e Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 29 Oct 2015 10:41:25 +0100
Subject: CLEANUP PROPOSITION: The 'pCIC' keyword from the 'Global Index' was
 removed.

We do not actually define the 'pCIC' concept in Chapter 4
so it does not make sense to keep an entry in the 'Global Index' for it.
---
 doc/refman/RefMan-cic.tex | 1 -
 1 file changed, 1 deletion(-)

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 6db02c0f24..38e7db18e5 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1,7 +1,6 @@
 \chapter[Calculus of Inductive Constructions]{Calculus of Inductive Constructions
 \label{Cic}
 \index{Cic@\textsc{CIC}}
-\index{pCic@p\textsc{CIC}}
 \index{Calculus of Inductive Constructions}}
 
 The underlying formal language of {\Coq} is a {\em Calculus of
-- 
cgit v1.2.3