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 /plugins/funind | |
| 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/funind')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 40abdb68b5..507ba19701 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1405,7 +1405,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false false)) true + with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false false)) Decl_kinds.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 6eabe6e871..0886e7f711 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -355,8 +355,8 @@ let ind2name = Id.of_string "__ind2" be co-inductive, and for the moment they must not be mutual either. *) let verify_inds mib1 mib2 = - if not mib1.mind_finite then error "First argument is coinductive"; - if not mib2.mind_finite then error "Second argument is coinductive"; + if mib1.mind_finite == Decl_kinds.CoFinite then error "First argument is coinductive"; + if mib2.mind_finite == Decl_kinds.CoFinite then error "Second argument is coinductive"; if not (Int.equal mib1.mind_ntypes 1) then error "First argument is mutual"; if not (Int.equal mib2.mind_ntypes 1) then error "Second argument is mutual"; () @@ -885,7 +885,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in let mie,impls = Command.interp_mutual_inductive indl [] - false (*FIXMEnon-poly *) false (* means not private *) true (* means: not coinductive *) in + false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls) |