diff options
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/library/global.ml b/library/global.ml index dfcd8c410..6548e6537 100644 --- a/library/global.ml +++ b/library/global.ml @@ -128,7 +128,9 @@ let mind_of_delta mind = let resolver,resolver_param = (delta_of_senv !global_env) in Mod_subst.mind_of_delta resolver_param (Mod_subst.mind_of_delta resolver mind) - + +let exists_label id = exists_label id !global_env + let start_library dir = let mp,newenv = start_library dir !global_env in global_env := newenv; |