diff options
Diffstat (limited to 'engine/uState.mli')
| -rw-r--r-- | engine/uState.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/engine/uState.mli b/engine/uState.mli index 7f2357a68..38af08f91 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -32,6 +32,8 @@ val of_context_set : Univ.ContextSet.t -> t val of_binders : Universes.universe_binders -> t +val universe_binders : t -> Universes.universe_binders + (** {5 Projections} *) val context_set : t -> Univ.ContextSet.t @@ -135,12 +137,12 @@ val normalize : t -> t Also return the association list of universe names and universes (including those not in [names]). *) val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t -> - Universes.universe_binders * Univ.UContext.t + Univ.UContext.t type universe_decl = (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl -val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.UContext.t +val check_univ_decl : t -> universe_decl -> Univ.UContext.t (** {5 TODO: Document me} *) |