diff options
| -rw-r--r-- | kernel/closure.ml | 2 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4103.v | 12 |
3 files changed, 15 insertions, 3 deletions
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)) 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 diff --git a/test-suite/bugs/closed/4103.v b/test-suite/bugs/closed/4103.v new file mode 100644 index 0000000000..92cc0279ac --- /dev/null +++ b/test-suite/bugs/closed/4103.v @@ -0,0 +1,12 @@ +Set Primitive Projections. + +CoInductive stream A := { hd : A; tl : stream A }. + +CoFixpoint ticks (n : nat) : stream unit := {| hd := tt; tl := ticks n |}. + +Lemma expand : exists n : nat, (ticks n) = (ticks n).(tl _). +Proof. + eexists. + (* Set Debug Tactic Unification. *) + (* Set Debug RAKAM. *) + reflexivity. |