diff options
| author | Arnaud Spiwack | 2014-09-03 11:40:27 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-04 10:25:54 +0200 |
| commit | b18b40878f071b6c7d67d1a2d031370f7a498d0b (patch) | |
| tree | 595398248a70dd2607c983c5dd3eb8913614b084 /pretyping | |
| parent | ac2fdfb222083faa9c3893194e020bed38555ddb (diff) | |
Print [Variant] types with the keyword [Variant].
Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
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 edd1080713..7ce6bc3e2f 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 913afb2191..4b6107c4ed 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 46f65271f4..d5dfd7bf00 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 |