diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 7 | ||||
| -rw-r--r-- | library/global.mli | 5 |
2 files changed, 12 insertions, 0 deletions
diff --git a/library/global.ml b/library/global.ml index 118a189c6c..7b69ca0a85 100644 --- a/library/global.ml +++ b/library/global.ml @@ -5,6 +5,7 @@ open Util open Term open Instantiate open Sign +open Environ open Safe_typing open Summary @@ -54,6 +55,12 @@ let import cenv = global_env := import cenv !global_env let id_of_global id = Environ.id_of_global (env_of_safe_env !global_env) id +(*s Function to get an environment from the constants part of the global + environment and a given context. *) + +let env_of_context hyps = + change_hyps (fun _ -> hyps) (env_of_safe_env !global_env) + (* Functions of [Inductive], composed with [lookup_mind_specif]. *) (* Rem:Cannot open Inductive to avoid clash with Inductive.lookup_mind_specif*) diff --git a/library/global.mli b/library/global.mli index e9a9503ff3..a59c998231 100644 --- a/library/global.mli +++ b/library/global.mli @@ -46,6 +46,11 @@ val import : compiled_env -> unit val id_of_global : global_reference -> identifier +(*s Function to get an environment from the constants part of the global + environment and a given context. *) + +val env_of_context : named_context -> env + (*s Re-exported functions of [Inductive], composed with [lookup_mind_specif]. *) |