aboutsummaryrefslogtreecommitdiff
path: root/API
diff options
context:
space:
mode:
Diffstat (limited to 'API')
-rw-r--r--API/API.mli4
1 files changed, 3 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli
index 6251bc18b8..3ed008ff5f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2781,6 +2781,8 @@ sig
end
type universe_constraints = Constraints.t
+ [@@ocaml.deprecated "Use Constraints.t"]
+
end
module UState :
@@ -3117,7 +3119,7 @@ sig
val fold : Evd.evar_map -> ('a -> constr -> 'a) -> 'a -> constr -> 'a
val existential_type : Evd.evar_map -> existential -> types
val iter : Evd.evar_map -> (constr -> unit) -> constr -> unit
- val eq_constr_universes : Evd.evar_map -> constr -> constr -> Universes.universe_constraints option
+ val eq_constr_universes : Evd.evar_map -> constr -> constr -> Universes.Constraints.t option
val eq_constr_nounivs : Evd.evar_map -> constr -> constr -> bool
val compare_constr : Evd.evar_map -> (constr -> constr -> bool) -> constr -> constr -> bool
val isApp : Evd.evar_map -> constr -> bool