diff options
Diffstat (limited to 'library/declare.mli')
| -rw-r--r-- | library/declare.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/declare.mli b/library/declare.mli index 94457a9f8..1a68f8e20 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -21,11 +21,11 @@ open Nametab open Decl_kinds (*i*) -(* This module provides the official functions to declare new variables, +(* This module provides the official functions to declare new variables, parameters, constants and inductive types. Using the following functions will add the entries in the global environment (module [Global]), will register the declarations in the library (module [Lib]) --- so that the - reset works properly --- and will fill some global tables such as + reset works properly --- and will fill some global tables such as [Nametab] and [Impargs]. *) open Nametab |