From 60cb1f81e475d4b0f044a56ec4de503e42bad99a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 29 Jan 2018 11:11:35 +0100
Subject: [cbv] Fix evaluation of cofixpoints under primitive projections.

Fixes #5286 (last remaining part).
---
 pretyping/cbv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 192eca63bb..e42576d95b 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -171,7 +171,7 @@ let fixp_reducible flgs ((reci,i),_) stk =
 let cofixp_reducible flgs _ stk =
   if red_set flgs fCOFIX then
     match stk with
-      | (CASE _ | APP(_,CASE _)) -> true
+      | (CASE _ | PROJ _ | APP(_,CASE _) | APP(_,PROJ _)) -> true
       | _ -> false
   else
     false
-- 
cgit v1.2.3