aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--library/globnames.ml8
-rw-r--r--library/globnames.mli8
2 files changed, 8 insertions, 8 deletions
diff --git a/library/globnames.ml b/library/globnames.ml
index 3befaa9a9..2d6afc857 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -14,10 +14,10 @@ open Libnames
(*s 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. *)
let isVarRef = function VarRef _ -> true | _ -> false
let isConstRef = function ConstRef _ -> true | _ -> false
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