diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 |
3 files changed, 4 insertions, 4 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 diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 913afb219..4b6107c4e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -441,7 +441,7 @@ let find_inductive env sigma c = let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in match kind_of_term t with | Ind ind - when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite -> + when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l) | _ -> raise Not_found @@ -449,7 +449,7 @@ let find_coinductive env sigma c = let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in match kind_of_term t with | Ind ind - when not (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite -> + when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l) | _ -> raise Not_found diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 46f65271f..d5dfd7bf0 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -461,7 +461,7 @@ let is_eta_constructor_app env f l1 = let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with | Some (exp,projs) when Array.length projs > 0 - && mib.Declarations.mind_finite -> + && mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> Array.length projs == Array.length l1 - mib.Declarations.mind_nparams | _ -> false) | _ -> false |