From cd31e372c6fb25769c26879f2f65f1937d098b87 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 4 Oct 2015 08:43:19 +0200
Subject: RefMan, ch. 4: Unify capitalization of "calculus of inductive
 constructions".

---
 doc/refman/RefMan-ext.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index a2be25c3ba..a718a26ea5 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -289,7 +289,7 @@ To deactivate the printing of projections, use
 
 The option {\tt Set Primitive Projections} turns on the use of primitive
 projections when defining subsequent records. Primitive projections
-extended the calculus of inductive constructions with a new binary term
+extended the Calculus of Inductive Constructions with a new binary term
 constructor {\tt r.(p)} representing a primitive projection p applied to
 a record object {\tt r} (i.e., primitive projections are always
 applied). Even if the record type has parameters, these do not appear at
-- 
cgit v1.2.3