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 /kernel/nativelambda.ml | |
| 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 'kernel/nativelambda.ml')
| -rw-r--r-- | kernel/nativelambda.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 16ca444e3a..34ed33f949 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -599,7 +599,7 @@ let rec lambda_of_constr env sigma c = { asw_ind = ind; asw_ci = ci; asw_reloc = tbl; - asw_finite = mib.mind_finite; + asw_finite = mib.mind_finite <> Decl_kinds.CoFinite; asw_prefix = prefix} in (* translation of the argument *) |