From 8a4a8758075e09da298762da1a035a5afac4d88b Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 21 Dec 2015 11:37:06 +0100
Subject: COMMENTS: added to the "Names.inductive" and "Names.constructor"
 types.

---
 kernel/names.ml | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

(limited to 'kernel/names.ml')

diff --git a/kernel/names.ml b/kernel/names.ml
index 0de752c7c5..d1e2c8afee 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -585,11 +585,16 @@ module Mindmap = HMap.Make(MutInd.CanOrd)
 module Mindset = Mindmap.Set
 module Mindmap_env = HMap.Make(MutInd.UserOrd)
 
-(** Beware: first inductive has index 0 *)
-(** Beware: first constructor has index 1 *)
-
-type inductive = MutInd.t * int
-type constructor = inductive * int
+(** Designation of a (particular) inductive type. *)
+type inductive = MutInd.t      (* the name of the inductive type *)
+               * int           (* the position of this inductive type
+                                  within the block of mutually-recursive inductive types.
+                                  BEWARE: indexing starts from 0. *)
+
+(** Designation of a (particular) constructor of a (particular) inductive type. *)
+type constructor = inductive   (* designates the inductive type *)
+                 * int         (* the index of the constructor
+                                  BEWARE: indexing starts from 1. *)
 
 let ind_modpath (mind,_) = MutInd.modpath mind
 let constr_modpath (ind,_) = ind_modpath ind
-- 
cgit v1.2.3