diff options
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index da39b1d3dd..00eb5c6d29 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1356,6 +1356,7 @@ Print Canonical Projections. \end{coq_example} \subsection{Implicit types of variables} +\comindex{Implicit Types} It is possible to bind variable names to a given type (e.g. in a development using arithmetic, it may be convenient to bind the names |