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.

---
 checker/inductive.ml | 6 ++++--
 kernel/inductive.ml  | 6 ++++--
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 909ecccaed..5825d1ab82 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -988,6 +988,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 _ -> anomaly (Pp.str "Section variable in Coqchk !")
 
 	| Sort _ -> assert (l = [])
@@ -997,8 +1001,6 @@ let check_one_fix renv recpos trees def =
 
         | (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 decr = 0 then
       check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index fbe0920bcf..52f578987e 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