diff options
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/global.mli b/library/global.mli index a06d4640e..6ca5bfb83 100644 --- a/library/global.mli +++ b/library/global.mli @@ -31,7 +31,7 @@ val env_is_empty : unit -> bool val universes : unit -> universes val named_context_val : unit -> Environ.named_context_val -val named_context : unit -> Sign.named_context +val named_context : unit -> Context.named_context val env_is_empty : unit -> bool |