diff options
| author | Maxime Dénès | 2017-12-11 11:35:17 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-11 11:35:17 +0100 |
| commit | a77f3a3e076e273af35ad520cae2eef0e3552811 (patch) | |
| tree | bedea2242a6c3f0e2deb6a2cd4f731f7c5014824 /engine/evd.mli | |
| parent | 5aaa240e4480ade7a5348e71a95fe3b2bc5a2c4e (diff) | |
| parent | 611da26d847888031cac4d6976b9e7e1e90cdc0e (diff) | |
Merge PR #6368: [api] Remove yet another type alias.
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index fb5a6cd16e..636bd1be11 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -208,7 +208,7 @@ val is_defined : evar_map -> Evar.t-> bool val is_undefined : evar_map -> Evar.t-> bool (** Whether an evar is not defined in an evarmap. *) -val add_constraints : evar_map -> Univ.constraints -> evar_map +val add_constraints : evar_map -> Univ.Constraint.t -> evar_map (** Add universe constraints in an evar map. *) val undefined_map : evar_map -> evar_info Evar.Map.t @@ -316,7 +316,7 @@ val whd_sort_variable : evar_map -> constr -> constr exception UniversesDiffer -val add_universe_constraints : evar_map -> Universes.universe_constraints -> evar_map +val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map (** Add the given universe unification constraints to the evar map. @raises UniversesDiffer in case a first-order unification fails. @raises UniverseInconsistency @@ -491,7 +491,7 @@ val univ_flexible_alg : rigid type 'a in_evar_universe_context = 'a * UState.t val evar_universe_context_set : UState.t -> Univ.ContextSet.t -val evar_universe_context_constraints : UState.t -> Univ.constraints +val evar_universe_context_constraints : UState.t -> Univ.Constraint.t val evar_context_universe_context : UState.t -> Univ.UContext.t [@@ocaml.deprecated "alias of UState.context"] @@ -513,7 +513,7 @@ val universe_of_name : evar_map -> Id.t -> Univ.Level.t val universe_binders : evar_map -> Universes.universe_binders val add_constraints_context : UState.t -> - Univ.constraints -> UState.t + Univ.Constraint.t -> UState.t val normalize_evar_universe_context_variables : UState.t -> |