diff options
Diffstat (limited to 'engine/uState.mli')
| -rw-r--r-- | engine/uState.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/engine/uState.mli b/engine/uState.mli index 4265f2b203..16fba41e06 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -80,9 +80,6 @@ val add_universe_constraints : t -> Universes.universe_constraints -> t (** {5 Names} *) -val add_universe_name : t -> Id.t -> Univ.Level.t -> t -(** Associate a human-readable name to a local variable. *) - val universe_of_name : t -> Id.t -> Univ.Level.t (** Retrieve the universe associated to the name. *) |