diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:27:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:46:52 +0100 |
| commit | 03e21974a3e971a294533bffb81877dc1bd270b6 (patch) | |
| tree | 1b37339378f6bc93288b61f707efb6b08f992dc5 /engine/uState.mli | |
| parent | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (diff) | |
[api] Move structures deprecated in the API to the core.
We do up to `Term` which is the main bulk of the changes.
Diffstat (limited to 'engine/uState.mli')
| -rw-r--r-- | engine/uState.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/engine/uState.mli b/engine/uState.mli index c44f2c1d7..b31e94b28 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -28,13 +28,13 @@ val is_empty : t -> bool val union : t -> t -> t -val of_context_set : Univ.universe_context_set -> t +val of_context_set : Univ.ContextSet.t -> t val of_binders : Universes.universe_binders -> t (** {5 Projections} *) -val context_set : t -> Univ.universe_context_set +val context_set : t -> Univ.ContextSet.t (** The local context of the state, i.e. a set of bound variables together with their associated constraints. *) @@ -54,7 +54,7 @@ val algebraics : t -> Univ.LSet.t val constraints : t -> Univ.constraints (** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *) -val context : t -> Univ.universe_context +val context : t -> Univ.UContext.t (** Shorthand for {!context_set} with {!Context_set.to_context}. *) (** {5 Constraints handling} *) @@ -79,7 +79,7 @@ val universe_of_name : t -> string -> Univ.Level.t (** {5 Unification} *) -val restrict : t -> Univ.universe_set -> t +val restrict : t -> Univ.LSet.t -> t type rigid = | UnivRigid @@ -89,7 +89,7 @@ val univ_rigid : rigid val univ_flexible : rigid val univ_flexible_alg : rigid -val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.universe_context_set -> t +val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t val merge_subst : t -> Universes.universe_opt_subst -> t val emit_side_effects : Safe_typing.private_constants -> t -> t @@ -130,12 +130,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 -> - (Id.t * Univ.Level.t) list * Univ.universe_context + (Id.t * Univ.Level.t) list * 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.universe_context +val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.UContext.t (** {5 TODO: Document me} *) |