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.

4 files changed, 8 insertions, 8 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);
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