diff options
| -rw-r--r-- | doc/RefMan-oth.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex index a8623f04f..e065d54ed 100644 --- a/doc/RefMan-oth.tex +++ b/doc/RefMan-oth.tex @@ -19,6 +19,7 @@ This is a synonym to {\tt Print {\qualid}} when {\qualid} denotes a global constant. \item {\tt About {\qualid}.} +\label{About} \comindex{About}\\ This displays various informations about the object denoted by {\qualid}: its kind (module, constant, assumption, inductive, |