aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/typeops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 09299f31d7..4f32fdce83 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -477,7 +477,7 @@ let rec execute env cstr =
let j' = execute env1 c3 in
judge_of_letin env name j1 j2 j'
- | Cast (c,k, t) ->
+ | Cast (c,k,t) ->
let cj = execute env c in
let tj = execute_type env t in
judge_of_cast env cj k tj