From a5feb9687819c5e7ef0db6e7b74d0e236a296674 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 21:01:57 +0200 Subject: Separate checking univ_decls and obtaining universe binder names. --- engine/uState.mli | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'engine/uState.mli') 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} *) -- cgit v1.2.3