COMMENTS: added to the "Names.inductive" and "Names.constructor" types.

1 files changed, 10 insertions, 5 deletions

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