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.

---
 pretyping/reductionops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 09eb38bd12..21f13a51f1 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -994,7 +994,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
     | CoFix cofix ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	match Stack.strip_app stack with
-	|args, (Stack.Case(ci, _, lf,_)::s') ->
+	|args, ((Stack.Case _ |Stack.Proj _)::s') ->
 	  reduce_and_refold_cofix whrec env cst_l cofix stack
 	|_ -> fold ()
       else fold ()
@@ -1073,7 +1073,7 @@ let local_whd_state_gen flags sigma =
     | CoFix cofix ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	match Stack.strip_app stack with
-	|args, (Stack.Case(ci, _, lf,_)::s') ->
+	|args, ((Stack.Case _ | Stack.Proj _)::s') ->
 	  whrec (contract_cofix cofix, stack)
 	|_ -> s
       else s
-- 
cgit v1.2.3