diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-04 21:16:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:05 +0100 |
| commit | 650ed1278160c2d6dae7914703c8755ab54e095c (patch) | |
| tree | 2c1b0200440ca8502a9653b8b9aece0ada8093db /doc/common | |
| parent | 75896eaaf60ce947e1fbc5a795ca5969bb1e4fae (diff) | |
RefMan, ch. 4: Reformulating introduction of the chapter on CIC, being
clearer that the version depends on the version of Coq.
Also renouncing to the "Predicative" and "(Co)" in the name, since
after all, usage seems to continue calling the language of Coq
Calculus of Inductive Constructions and to consider the Set
predicative vs Set impredicative, as well as the presence of
coinduction, as flavors of the CIC.
Diffstat (limited to 'doc/common')
| -rw-r--r-- | doc/common/macros.tex | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 0e820008e..573c3c812 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -97,8 +97,7 @@ \newcommand{\camlpppp}{\textsc{Camlp4}} \newcommand{\emacs}{\textsc{GNU Emacs}} \newcommand{\ProofGeneral}{\textsc{Proof General}} -\newcommand{\CIC}{\pCIC} -\newcommand{\pCIC}{p\textsc{Cic}} +\newcommand{\CIC}{\textsc{Cic}} \newcommand{\iCIC}{\textsc{Cic}} \newcommand{\FW}{\ensuremath{F_{\omega}}} \newcommand{\Program}{\textsc{Program}} |