diff options
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 97ac88183..9547231af 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -10,10 +10,13 @@ open Util open Pp open Names open Term +open Context open Sign open Environ open Locus +(** TODO: merge this with Term *) + (** Universes *) val new_univ_level : unit -> Univ.universe_level val new_univ : unit -> Univ.universe |