aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/subtyping.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/subtyping.mli
parent319a3c230e9f9ec5a8a5bea9e07b6b8d17444ac9 (diff)
[api] Remove yet another type alias.
Diffstat (limited to 'kernel/subtyping.mli')
-rw-r--r--kernel/subtyping.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli
index b24c20aa0..67df3759e 100644
--- a/kernel/subtyping.mli
+++ b/kernel/subtyping.mli
@@ -10,4 +10,4 @@ open Univ
open Declarations
open Environ
-val check_subtypes : env -> module_type_body -> module_type_body -> constraints
+val check_subtypes : env -> module_type_body -> module_type_body -> Constraint.t