diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-08 12:44:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-08 12:44:59 +0000 |
| commit | 6b59b0f2a993c56cf0adc1d052a98b0df334a0f7 (patch) | |
| tree | 80f21c09f04011cf0087b8d4b2ebdd519c9a591c /library/global.mli | |
| parent | 6db6c3b0e7a9323fdebfcf3be188fc7b0e04da8f (diff) | |
Rely on kernel to know if a name is already used so as to be consistent with it.
Maybe could we keep only the kernel check, but message would
certainly need to be reformulated then.
For instance, the message was previously different for an attempt to
redefine a name whether this name was in the same section or not.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14528 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/library/global.mli b/library/global.mli index 9beb535d5..7859c51ef 100644 --- a/library/global.mli +++ b/library/global.mli @@ -87,6 +87,7 @@ val lookup_module : module_path -> module_body val lookup_modtype : module_path -> module_type_body val constant_of_delta : constant -> constant val mind_of_delta : mutual_inductive -> mutual_inductive +val exists_label : label -> bool (** Compiled modules *) val start_library : dir_path -> module_path |