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 /plugins/xml | |
| 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/xml')
| -rw-r--r-- | plugins/xml/xmlcommand.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index ef5e18201..d65e6f317 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -272,7 +272,7 @@ let theory_output_string ?(do_not_quote = false) s = let kind_of_inductive isrecord kn = "DEFINITION", - if (fst (Global.lookup_inductive (kn,0))).Declarations.mind_finite + if (fst (Global.lookup_inductive (kn,0))).Declarations.mind_finite <> Decl_kinds.CoFinite then begin match isrecord with | Declare.KernelSilent -> "Record" @@ -389,7 +389,7 @@ let print internal glob_ref kind xml_library_root = Declarations.mind_packets=packs ; Declarations.mind_hyps=hyps; Declarations.mind_finite=finite} = mib in - Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite + Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps (finite<>Decl_kinds.CoFinite) | Globnames.ConstructRef _ -> Errors.error ("a single constructor cannot be printed in XML") in |