From 3be70f39bbaba7c7edb5e5f3e26d4f952c06824e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 18 May 2018 16:00:17 +0200
Subject: Fix #7539: Checker does not properly handle negative coinductive
 types.

The reduction machine of the checker was not taking into account the fact
that cofixpoints needed to be unfolded when applied against a projection.
---
 checker/closure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/closure.ml b/checker/closure.ml
index bfba6c161..3f6dfd30f 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -762,7 +762,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, (((ZcaseT _)::_) as stk')) ->
+          (_, args, (((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