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 /kernel/names.mli | |
parent | 730e8b8445c6ff28540aff4a052e19b90159a86d (diff) |
COMMENTS: added to the "Names.inductive" and "Names.constructor" types.
Diffstat (limited to 'kernel/names.mli')
-rw-r--r-- | kernel/names.mli | 15 |
1 files changed, 10 insertions, 5 deletions
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 |