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

1 files changed, 10 insertions, 5 deletions

diff --git a/kernel/names.mli b/kernel/names.mli
index b128fe3351..d424552e44 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 : Map.S 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 : Map.S with type key = inductive
 module Constrmap : Map.S with type key = constructor