COMMENTS: added to some variants of "Globalnames.global_reference" type.

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