aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.mli
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-09 23:14:19 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-09 23:21:29 +0100
commit611da26d847888031cac4d6976b9e7e1e90cdc0e (patch)
treeafe5585510610fc26e7fb4381b322b7cc1323c91 /kernel/safe_typing.mli
parent319a3c230e9f9ec5a8a5bea9e07b6b8d17444ac9 (diff)
[api] Remove yet another type alias.
Diffstat (limited to 'kernel/safe_typing.mli')
-rw-r--r--kernel/safe_typing.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 0bfe07486..a30bb37e6 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -139,7 +139,7 @@ val push_context :
bool -> Univ.UContext.t -> safe_transformer0
val add_constraints :
- Univ.constraints -> safe_transformer0
+ Univ.Constraint.t -> safe_transformer0
(* (\** Generator of universes *\) *)
(* val next_universe : int safe_transformer *)