diff options
| author | Pierre-Marie Pédrot | 2015-10-19 18:18:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-19 18:18:34 +0200 |
| commit | c7dcb76ffff6b12b031e906b002b4d76c1aaea50 (patch) | |
| tree | 8d5115258c3b7042767e45d742e2800dab209822 /kernel/typeops.ml | |
| parent | 666568377cbe1c18ce479d32f6359aa61af6d553 (diff) | |
| parent | 50a574f8b3e7f29550d7abf600d92eb43e7f8ef6 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 2 |
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 |