diff options
| author | Matej Kosik | 2015-10-30 16:50:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:10 +0100 |
| commit | c5b3e7ff66e1675aaec7be5e0ee6772e88250991 (patch) | |
| tree | 461756dd215bc4d4cb83eb66d190de22b8220e75 | |
| parent | 73985c85792da06857199311834962f6a417e71c (diff) | |
ENH: the concept of 'inductive declaration' was added to the 'Global Index'
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 764f1189ba..7fd5b23039 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -519,7 +519,7 @@ reductions or any combination of those can also be defined. A (possibly mutual) inductive definition is specified by giving the names and types of the inductive types to be defined and the names and types of the constructors of the inductive types. -An inductive declaration in the global environment can +An {\em inductive declaration\index{declaration!inductive}} in the global environment can consequently be represented with two local contexts, one for the types one for the constructors. |