aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-cic.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
-rw-r--r--doc/refman/RefMan-cic.tex1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index ad795d4064..0dbfe05d48 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -2,6 +2,7 @@
\label{Cic}
\index{Cic@\textsc{CIC}}
\index{Calculus of Inductive Constructions}}
+%HEVEA\cutname{cic.html}
The underlying formal language of {\Coq} is a {\em Calculus of
Inductive Constructions} (\CIC) whose inference rules are presented in