From b18b40878f071b6c7d67d1a2d031370f7a498d0b Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 3 Sep 2014 11:40:27 +0200 Subject: 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. --- plugins/extraction/extraction.ml | 4 ++-- plugins/funind/glob_term_to_relation.ml | 2 +- plugins/funind/merge.ml | 6 +++--- plugins/xml/xmlcommand.ml | 4 ++-- 4 files changed, 8 insertions(+), 8 deletions(-) (limited to 'plugins') 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); diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 40abdb68b..507ba1970 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 6eabe6e87..0886e7f71 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) 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 -- cgit v1.2.3