diff options
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 9c7e7d1df4..fc511a45c1 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -994,7 +994,8 @@ declaration is added to the context. An absolute name is called {\it visible} from a given short or partially qualified name when this latter name is enough to denote it. This means that the short or partially qualified name is mapped to the absolute name in {\Coq} name -table. +table. Definitions flagged as {\tt Local} are only accessible with their +fully qualified name (see \ref{Definition}). A similar table exists for library file names. It is updated by the vernacular commands {\tt Add LoadPath} and {\tt Add Rec LoadPath} (or |