diff options
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/library/global.ml b/library/global.ml index 9238b6e85c..0fc1852cb9 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,7 +6,7 @@ open Generic open Term open Instantiate open Sign -open Typing +open Safe_typing open Summary (* We introduce here the global environment of the system, and we declare it @@ -28,6 +28,7 @@ let _ = let universes () = universes !global_env let context () = context !global_env +let var_context () = var_context !global_env let push_var idc = global_env := push_var idc !global_env let push_rel nac = global_env := push_rel nac !global_env |