diff options
| author | Matej Kosik | 2015-12-21 11:37:06 +0100 |
|---|---|---|
| committer | Matej Kosik | 2015-12-22 16:25:20 +0100 |
| commit | e1ac3467db26f9bcc09f12989eeb8379c4fc5817 (patch) | |
| tree | e9c46f9944c414cda11513188903839131b9c582 /kernel | |
| parent | b88929d9d8de179a7e356cf9cbe2afef76f905a3 (diff) | |
COMMENTS: added to the "Names.inductive" and "Names.constructor" types.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 15 | ||||
| -rw-r--r-- | kernel/names.mli | 15 |
2 files changed, 20 insertions, 10 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 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 |