From 650ed1278160c2d6dae7914703c8755ab54e095c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 4 Oct 2015 21:16:17 +0200 Subject: 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. --- doc/common/macros.tex | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'doc/common') 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}} -- cgit v1.2.3