aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/globnames.ml2
-rw-r--r--library/globnames.mli2
2 files changed, 2 insertions, 2 deletions
diff --git a/library/globnames.ml b/library/globnames.ml
index 8b1a51377..2fa3adba2 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -15,7 +15,7 @@ open Mod_subst
open Libnames
(*s Global reference is a kernel side type for all references together *)
-type global_reference =
+type global_reference = Names.global_reference =
| VarRef of variable (** A reference to the section-context. *)
| ConstRef of Constant.t (** A reference to the environment. *)
| IndRef of inductive (** A reference to an inductive type. *)
diff --git a/library/globnames.mli b/library/globnames.mli
index 017b7386d..f2b88b870 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -14,7 +14,7 @@ open Constr
open Mod_subst
(** {6 Global reference is a kernel side type for all references together } *)
-type global_reference =
+type global_reference = Names.global_reference =
| VarRef of variable (** A reference to the section-context. *)
| ConstRef of Constant.t (** A reference to the environment. *)
| IndRef of inductive (** A reference to an inductive type. *)