aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/globnames.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/globnames.mli')
-rw-r--r--library/globnames.mli8
1 files changed, 4 insertions, 4 deletions
diff --git a/library/globnames.mli b/library/globnames.mli
index f94f6216f..f4956e3df 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