From 35e47b6be8d9e97b58464daccc28d179951b5e47 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 17 Dec 2013 16:12:50 +0100
Subject: Tentative fix of the guardedness checker by Christine and me. All
 stdlib and test-suite pass.

---
 kernel/term_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/term_typing.ml')

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
-- 
cgit v1.2.3