From 51b4d0cdad77f2874bd481dabd32e0772563dc3f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 3 Mar 2015 15:47:24 +0100
Subject: Fix bug #4103: forgot to allow unfolding projections of cofixpoints
 like cases, in some cases.

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

(limited to 'kernel')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 6824c399e6..ea9b2755f2 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -924,7 +924,7 @@ let rec knr info m stk =
         | (_,args,s) -> (m,args@s))
   | FCoFix _ when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
-          (_, args, (((Zcase _|ZcaseT _)::_) as stk')) ->
+          (_, args, (((Zcase _|ZcaseT _|Zproj _)::_) as stk')) ->
             let (fxe,fxbd) = contract_fix_vect m.term in
             knit info fxe fxbd (args@stk')
         | (_,args,s) -> (m,args@s))
-- 
cgit v1.2.3