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 ++++++++++-----
 kernel/names.mli | 15 ++++++++++-----
 2 files changed, 20 insertions(+), 10 deletions(-)

(limited to 'kernel')

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
diff --git a/kernel/names.mli b/kernel/names.mli
index 38a51a3927..df296ab6c6 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -411,11 +411,16 @@ module Mindset : CSig.SetS with type elt = MutInd.t
 module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset
 module Mindmap_env : CSig.MapS with type key = MutInd.t
 
-(** Beware: first inductive has index 0 *)
-type inductive = MutInd.t * int
-
-(** Beware: first constructor has index 1 *)
-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. *)
 
 module Indmap : CSig.MapS with type key = inductive
 module Constrmap : CSig.MapS with type key = constructor
-- 
cgit v1.2.3