From ba00867d515624aee734d998bfbe3880f559d907 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 25 Jul 2016 16:39:34 +0200 Subject: Fix bug #4876: critical bug in guard condition checker. --- kernel/inductive.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index fbe0920bc..52f578987 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1010,6 +1010,10 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l + | Proj (p, c) -> + List.iter (check_rec_call renv []) l; + check_rec_call renv [] c + | Var id -> begin match pi2 (lookup_named id renv.env) with @@ -1028,8 +1032,6 @@ let check_one_fix renv recpos trees def = | (Evar _ | Meta _) -> () | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) - - | Proj (p, c) -> check_rec_call renv [] c and check_nested_fix_body renv decr recArgsDecrArg body = if Int.equal decr 0 then -- cgit v1.2.3