From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- library/globnames.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'library/globnames.mli') diff --git a/library/globnames.mli b/library/globnames.mli index f94f6216..f4956e3d 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 -- cgit v1.2.3