diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-26 16:03:12 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-26 16:03:12 +0000 |
commit | f22d5b55021fcf5fb11fa9d4fce3a7b8d9bc532f (patch) | |
tree | 24438c2eb0ca59ebe62f90c39e11bc2918e9cf4a /kernel/declarations.mli | |
parent | 263ec91e6664a9f1f8823c791690cb5ddf43c547 (diff) |
Module names and constant/inductive names are now in two separate namespaces
We now accept the following code: Definition E := 0. Module E. End E.
Techically, we simply allow the same label to occur at most twice in
a structure_body, which is a (label * structure_field_body) list).
These two label occurences should not be at the same level of fields
(e.g. a SFBmodule and a SFBmind are ok, but not two SFBmodule's or
a SFBmodule and a SFBmodtype). Gain : a minimal amount of code change.
Drawback : no more simple List.assoc or equivalent should be performed
on a structure_body ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15088 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/declarations.mli')
-rw-r--r-- | kernel/declarations.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 5b800edec..7cf74ba3c 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -192,6 +192,10 @@ type structure_field_body = | SFBmodule of module_body | SFBmodtype of module_type_body +(** NB: we may encounter now (at most) twice the same label in + a [structure_body], once for a module ([SFBmodule] or [SFBmodtype]) + and once for an object ([SFBconst] or [SFBmind]) *) + and structure_body = (label * structure_field_body) list and struct_expr_body = |