diff options
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b2b6df3929..0ad03d417f 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -58,7 +58,7 @@ let handle_side_effects env body side_eff = Name (id_of_string name) in let rec sub c i x = match kind_of_term x with | Const c' when eq_constant c c' -> mkRel i - | _ -> map_constr_with_binders ((+) 1) (sub c) i x in + | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub c i x) i x in let fix_body (c,cb) t = match cb.const_body with | Undef _ -> assert false |