Tentative fix of the guardedness checker by Christine and me. All stdlib and test-suite pass.

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