diff options
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index d3fd22c01e..9f1c228a00 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -22,6 +22,7 @@ val empty_env : unsafe_env val universes : unsafe_env -> universes val context : unsafe_env -> context +val var_context : unsafe_env -> var_context val push_var : identifier * typed_type -> unsafe_env -> unsafe_env val change_hyps : |