diff options
| -rw-r--r-- | doc/RefMan-gal.tex | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex index 7fa4784911..57080a5a35 100644 --- a/doc/RefMan-gal.tex +++ b/doc/RefMan-gal.tex @@ -329,8 +329,11 @@ chapter \ref{Addoc-syntax}. %%%%%%% \subsection{Qualified identifiers and simple identifiers} +\label{qualid}\label{ident} -{\em Qualified identifiers} ({\qualid}) denote {\em constants}, {\em inductive +{\em Qualified identifiers} ({\qualid}) denote {\em global constants} +(definitions, lemmas, theorems, remarks or facts), {\em global +variables} (parameters or axioms), {\em inductive types} or {\em constructors of inductive types}. {\em Simple identifiers} (or shortly {\em identifiers}) are a syntactic subset of qualified identifiers. Identifiers may also |