diff options
| author | Matthieu Sozeau | 2015-03-03 15:47:24 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-03-03 15:49:42 +0100 |
| commit | 51b4d0cdad77f2874bd481dabd32e0772563dc3f (patch) | |
| tree | ec813c0fc816ca1446ef70e68151cdb889646f58 /pretyping | |
| parent | ac62cda8a4f488b94033b108c37556877232137a (diff) | |
Fix bug #4103: forgot to allow unfolding projections of cofixpoints like
cases, in some cases.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |