diff options
| author | Gaëtan Gilbert | 2017-09-09 14:54:42 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2017-09-19 10:28:03 +0200 |
| commit | 3c964a60d698134c21adc77cbb69ce1528350682 (patch) | |
| tree | 61d9fff65aaf7d6d844eef0a6c251bdd8f90e53e | |
| parent | cd29948855c2cbd3f4065170e41f8dbe625e1921 (diff) | |
Document UState.universe_context.
| -rw-r--r-- | engine/uState.mli | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/engine/uState.mli b/engine/uState.mli index 21145e7e67..c44f2c1d74 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -118,8 +118,17 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst val normalize : t -> t -(** {5 TODO: Document me} *) +(** [universe_context names extensible ctx] + + Return a universe context containing the local universes of [ctx] + and their constraints. The universes corresponding to [names] come + first in the order defined by that list. + + If [extensible] is false, check that the universes of [names] are + the only local universes. + 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 -> (Id.t * Univ.Level.t) list * Univ.universe_context @@ -128,6 +137,8 @@ type universe_decl = val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.universe_context +(** {5 TODO: Document me} *) + val update_sigma_env : t -> Environ.env -> t (** {5 Pretty-printing} *) |