aboutsummaryrefslogtreecommitdiff
path: root/engine/eConstr.mli
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-12-09 23:14:19 +0100
committerEmilio Jesus Gallego Arias2017-12-09 23:21:29 +0100
commit611da26d847888031cac4d6976b9e7e1e90cdc0e (patch)
treeafe5585510610fc26e7fb4381b322b7cc1323c91 /engine/eConstr.mli
parent319a3c230e9f9ec5a8a5bea9e07b6b8d17444ac9 (diff)
[api] Remove yet another type alias.
Diffstat (limited to 'engine/eConstr.mli')
-rw-r--r--engine/eConstr.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 3e6a13f709..771dbb8e88 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -187,9 +187,9 @@ val whd_evar : Evd.evar_map -> constr -> constr
val eq_constr : Evd.evar_map -> t -> t -> bool
val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
-val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option
-val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option
-val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.universe_constraints option
+val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option
+val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option
+val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
(** {6 Iterators} *)