aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/typeops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/typeops.mli')
-rw-r--r--kernel/typeops.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index a537d793e..ed90c393e 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -69,8 +69,8 @@ val judge_of_letin :
(*s Type of a cast. *)
val judge_of_cast :
- env -> unsafe_judgment -> unsafe_type_judgment
- -> unsafe_judgment * constraints
+ env -> unsafe_judgment -> cast_kind -> unsafe_type_judgment ->
+ unsafe_judgment * constraints
(*s Inductive types. *)