aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2016-07-25 16:39:34 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2016-07-25 16:40:58 +0200
commitba00867d515624aee734d998bfbe3880f559d907 (patch)
treea63e6cd8e7e65244eb1ed1a724967874914e17b1 /kernel
parente10c9eed42e9cfc843a6cb2d48fa175c1be98741 (diff)
Fix bug #4876: critical bug in guard condition checker.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/inductive.ml6
1 files changed, 4 insertions, 2 deletions
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