diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-04 08:43:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:05 +0100 |
| commit | cd31e372c6fb25769c26879f2f65f1937d098b87 (patch) | |
| tree | 67764ca15d823cabe62010870d5ab16d6712180c /doc/refman/RefMan-ext.tex | |
| parent | ef7264aa6106d0257e1a34f4ecf765279d9b602e (diff) | |
RefMan, ch. 4: Unify capitalization of "calculus of inductive constructions".
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index a2be25c3b..a718a26ea 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 |