diff options
author | 2014-09-03 11:40:27 +0200 | |
---|---|---|
committer | 2014-09-04 10:25:54 +0200 | |
commit | b18b40878f071b6c7d67d1a2d031370f7a498d0b (patch) | |
tree | 595398248a70dd2607c983c5dd3eb8913614b084 /plugins/extraction/extraction.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 'plugins/extraction/extraction.ml')
-rw-r--r-- | plugins/extraction/extraction.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index d2e95a74b..bbbc9bce7 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -220,7 +220,7 @@ let eq_record x y = let mib_equal m1 m2 = Array.equal oib_equal m1.mind_packets m1.mind_packets && eq_record m1.mind_record m2.mind_record && - (m1.mind_finite : bool) == m2.mind_finite && + (m1.mind_finite : Decl_kinds.recursivity_kind) == m2.mind_finite && Int.equal m1.mind_ntypes m2.mind_ntypes && List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps && Int.equal m1.mind_nparams m2.mind_nparams && @@ -437,7 +437,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let ip = (kn, 0) in let r = IndRef ip in if is_custom r then raise (I Standard); - if not mib.mind_finite then raise (I Coinductive); + if mib.mind_finite == Decl_kinds.CoFinite then raise (I Coinductive); if not (Int.equal mib.mind_ntypes 1) then raise (I Standard); let p,u = packets.(0) in if p.ip_logical then raise (I Standard); |