diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 9db8c8328b..b9f0ab9f53 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -131,9 +131,9 @@ inconsistency} error (see also Section~\ref{PrintingUniverses}). \subsection{Terms} \label{cic:terms} -Terms are built from sorts, variables, constant, +Terms are built from sorts, variables, constants, %constructors, inductive types, -abstraction, application, local definitions, +abstractions, applications, local definitions, %case analysis, fixpoints, cofixpoints and products. |