diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-16 15:24:18 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-18 15:58:14 +0100 |
| commit | 9e8a9ab17d4467a4aa40f31eaef0800703d31418 (patch) | |
| tree | 6f6d7e49900b90d9dc9823b24fce7d355c038aed /library/globnames.mli | |
| parent | e4423ce78823ad9dd8c726e31de712e67a91893a (diff) | |
COMMENTS: added to some variants of "Globalnames.global_reference" type.
Diffstat (limited to 'library/globnames.mli')
| -rw-r--r-- | library/globnames.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/globnames.mli b/library/globnames.mli index 253c20baa..a401046b4 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -13,10 +13,10 @@ open Mod_subst (** {6 Global reference is a kernel side type for all references together } *) type global_reference = - | VarRef of variable - | ConstRef of constant - | IndRef of inductive - | ConstructRef of constructor + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of constant (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) val isVarRef : global_reference -> bool val isConstRef : global_reference -> bool |