diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index edd108071..7ce6bc3e2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -762,7 +762,7 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (projs, pbs) when Array.length projs > 0 - && mib.Declarations.mind_finite -> + && mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in |