aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2015-12-16 15:24:18 +0100
committerGravatar Matej Kosik <m4tej.kosik@gmail.com>2015-12-18 15:58:14 +0100
commit9e8a9ab17d4467a4aa40f31eaef0800703d31418 (patch)
tree6f6d7e49900b90d9dc9823b24fce7d355c038aed /library
parente4423ce78823ad9dd8c726e31de712e67a91893a (diff)
COMMENTS: added to some variants of "Globalnames.global_reference" type.
Diffstat (limited to 'library')
-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