diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-09 23:14:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-09 23:21:29 +0100 |
| commit | 611da26d847888031cac4d6976b9e7e1e90cdc0e (patch) | |
| tree | afe5585510610fc26e7fb4381b322b7cc1323c91 /kernel/environ.mli | |
| parent | 319a3c230e9f9ec5a8a5bea9e07b6b8d17444ac9 (diff) | |
[api] Remove yet another type alias.
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 652ed0f9f..7cc541258 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -152,9 +152,9 @@ exception NotEvaluableConst of const_evaluation_result val constant_value : env -> Constant.t puniverses -> constr constrained val constant_type : env -> Constant.t puniverses -> types constrained -val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.constraints) option +val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.Constraint.t) option val constant_value_and_type : env -> Constant.t puniverses -> - constr option * types * Univ.constraints + constr option * types * Univ.Constraint.t (** The universe context associated to the constant, empty if not polymorphic *) val constant_context : env -> Constant.t -> Univ.AUContext.t @@ -203,10 +203,10 @@ val lookup_modtype : ModPath.t -> env -> module_type_body (** Add universe constraints to the environment. @raises UniverseInconsistency *) -val add_constraints : Univ.constraints -> env -> env +val add_constraints : Univ.Constraint.t -> env -> env (** Check constraints are satifiable in the environment. *) -val check_constraints : Univ.constraints -> env -> bool +val check_constraints : Univ.Constraint.t -> env -> bool val push_context : ?strict:bool -> Univ.UContext.t -> env -> env val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env val push_constraints_to_env : 'a Univ.constrained -> env -> env |