diff options
| author | Matej Kosik | 2015-10-29 10:41:25 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:09 +0100 |
| commit | 47c235b94e8870043deb04b65aad08eac8f7ae3e (patch) | |
| tree | 7e6413d994001f43c252164c6088b31e6a910dcf | |
| parent | cf7fb536777674b093ee1c5ac33126f75a55e12b (diff) | |
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.
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 1 |
1 files changed, 0 insertions, 1 deletions
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 |