diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-21 11:37:06 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-11 10:00:45 +0100 |
| commit | 8a4a8758075e09da298762da1a035a5afac4d88b (patch) | |
| tree | 4c3c05931f54a5455e6c5a993e839a5ac7716ce8 | |
| parent | 730e8b8445c6ff28540aff4a052e19b90159a86d (diff) | |
COMMENTS: added to the "Names.inductive" and "Names.constructor" types.
| -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 0de752c7c..d1e2c8afe 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 38a51a392..df296ab6c 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 |