diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-03 11:40:27 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-04 10:25:54 +0200 |
| commit | b18b40878f071b6c7d67d1a2d031370f7a498d0b (patch) | |
| tree | 595398248a70dd2607c983c5dd3eb8913614b084 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/command.mli | 4 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 4 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
4 files changed, 6 insertions, 6 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index d14af7394..bd6da2dbe 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -90,7 +90,7 @@ type one_inductive_impls = val interp_mutual_inductive : structured_inductive_expr -> decl_notation list -> polymorphic -> - private_flag -> bool(*finite*) -> + private_flag -> Decl_kinds.recursivity_kind -> mutual_inductive_entry * one_inductive_impls list (** Registering a mutual inductive definition together with its @@ -104,7 +104,7 @@ val declare_mutual_inductive_with_eliminations : val do_mutual_inductive : (one_inductive_expr * decl_notation list) list -> polymorphic -> - private_flag -> bool -> unit + private_flag -> Decl_kinds.recursivity_kind -> unit (** {6 Fixpoints and cofixpoints} *) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index b422e67b1..7db71c097 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -232,7 +232,7 @@ let declare_one_induction_scheme ind = let declare_induction_schemes kn = let mib = Global.lookup_mind kn in - if mib.mind_finite then begin + if mib.mind_finite <> Decl_kinds.CoFinite then begin for i = 0 to Array.length mib.mind_packets - 1 do declare_one_induction_scheme (kn,i); done; @@ -242,7 +242,7 @@ let declare_induction_schemes kn = let declare_eq_decidability_gen internal names kn = let mib = Global.lookup_mind kn in - if mib.mind_finite then + if mib.mind_finite <> Decl_kinds.CoFinite then ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn) let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *) diff --git a/toplevel/record.ml b/toplevel/record.ml index fedf63eed..3134a6be6 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -344,7 +344,7 @@ let declare_structure finite infer poly ctx id idbuild paramimpls params arity f let mie = { mind_entry_params = List.map degenerate_decl params; mind_entry_record = Some !primitive_flag; - mind_entry_finite = finite != CoFinite; + mind_entry_finite = finite; mind_entry_inds = [mie_ind]; mind_entry_polymorphic = poly; mind_entry_private = None; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4f6b2d5f7..9cb88f541 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -556,7 +556,7 @@ let vernac_inductive poly lo finite infer indl = | _ -> Errors.error "Cannot handle mutually (co)inductive records." in let indl = List.map unpack indl in - do_mutual_inductive indl poly lo (finite != CoFinite) + do_mutual_inductive indl poly lo finite let vernac_fixpoint locality poly local l = let local = enforce_locality_exp locality local in |