From 36b75df8ad9b118648ff0c295a097e71775b7656 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Tue, 25 Oct 2016 15:16:42 +0200
Subject: COMMENT: Declarations.constant_def

---
 kernel/declarations.mli | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index fe2fa6d7f3..7821ea20ff 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -58,10 +58,11 @@ type projection_body = {
   proj_body : constr; (* For compatibility with VMs only, the match version *)
 }
 
+(* Global declarations (i.e. constants) can be either: *)
 type constant_def =
-  | Undef of inline
-  | Def of constr Mod_subst.substituted
-  | OpaqueDef of Opaqueproof.opaque
+  | Undef of inline                       (** a global assumption *)
+  | Def of constr Mod_subst.substituted   (** or a transparent global definition *)
+  | OpaqueDef of Opaqueproof.opaque       (** or an opaque global definition *)
 
 type constant_universes = Univ.universe_context
 
-- 
cgit v1.2.3