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.

24 files changed, 61 insertions, 39 deletions

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index bf9d2c0b9..87c8cb04d 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -111,10 +111,19 @@ let type_of_global_ref gr =
     | Globnames.IndRef ind ->
 	let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
 	  if mib.Declarations.mind_record <> None then
-	    if mib.Declarations.mind_finite then "rec"
-	    else "corec"
-	  else if mib.Declarations.mind_finite then "ind"
-	  else "coind"
+            let open Decl_kinds in
+            begin match mib.Declarations.mind_finite with
+            | Finite -> "indrec"
+            | BiFinite -> "rec"
+	    | CoFinite -> "corec"
+            end
+	  else
+            let open Decl_kinds in
+            begin match mib.Declarations.mind_finite with
+            | Finite -> "ind"
+            | BiFinite -> "variant"
+	    | CoFinite -> "coind"
+            end
     | Globnames.ConstructRef _ -> "constr"
 
 let remove_sections dir =
diff --git a/kernel/closure.ml b/kernel/closure.ml
index fcbe939a9..d0a9ffd64 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -867,7 +867,7 @@ let eta_expand_ind_stacks env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
     | Some (projs,pbs) when Array.length projs > 0 
-      && mib.Declarations.mind_finite -> 
+      && mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
 	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
       let pars = mib.Declarations.mind_nparams in
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 2c516cafd..6b3f6c72f 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -158,7 +158,7 @@ type mutual_inductive_body = {
 	In the case it is primitive we get its projection names and checked
 	projection bodies, otherwise both arrays are empty. *)
 
-    mind_finite : bool;  (** Whether the type is inductive or coinductive *)
+    mind_finite : Decl_kinds.recursivity_kind;  (** Whether the type is inductive or coinductive *)
 
     mind_ntypes : int;  (** Number of types in the block *)
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 2d7b7bb0f..bf47ff90e 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -44,7 +44,7 @@ type mutual_inductive_entry = {
   mind_entry_record : bool option; 
   (** Some true: primitive record
       Some false: non-primitive record *)
-  mind_entry_finite : bool;
+  mind_entry_finite : Decl_kinds.recursivity_kind;
   mind_entry_params : (Id.t * local_entry) list;
   mind_entry_inds : one_inductive_entry list;
   mind_entry_polymorphic : bool;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 189c2f4d2..6975544ac 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -38,14 +38,14 @@ let find_inductive env c =
   let (t, l) = decompose_app (whd_betadeltaiota env c) in
   match kind_of_term t with
     | Ind ind
-        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite -> (ind, l)
+        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l)
     | _ -> raise Not_found
 
 let find_coinductive env c =
   let (t, l) = decompose_app (whd_betadeltaiota env c) in
   match kind_of_term t with
     | Ind ind
-        when not (fst (lookup_mind_specif env (out_punivs ind))).mind_finite -> (ind, l)
+        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l)
     | _ -> raise Not_found
 
 let inductive_params (mib,_) = mib.mind_nparams
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 16ca444e3..34ed33f94 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -599,7 +599,7 @@ let rec lambda_of_constr env sigma c =
 	    { asw_ind = ind;
           asw_ci = ci;
           asw_reloc = tbl; 
-          asw_finite = mib.mind_finite;
+          asw_finite = mib.mind_finite <> Decl_kinds.CoFinite;
           asw_prefix = prefix}
       in
       (* translation of the argument *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 61420d7ca..f1402a3db 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -168,7 +168,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
       (arities_of_specif (mind,u) (mib2,p2))
   in
   let check f test why = if not (test (f mib1) (f mib2)) then error (why (f mib2)) in
-  check (fun mib -> mib.mind_finite) (==) (fun x -> FiniteInductiveFieldExpected x);
+  check (fun mib -> mib.mind_finite<>Decl_kinds.CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x);
   check (fun mib -> mib.mind_ntypes) Int.equal (fun x -> InductiveNumbersFieldExpected x);
   assert (List.is_empty mib1.mind_hyps && List.is_empty mib2.mind_hyps);
   assert (Array.length mib1.mind_packets >= 1
diff --git a/library/declare.ml b/library/declare.ml
index 6f0ead941..94239d0bf 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -372,7 +372,7 @@ let dummy_one_inductive_entry mie = {
 let dummy_inductive_entry (_,m) = ([],{
   mind_entry_params = [];
   mind_entry_record = None;
-  mind_entry_finite = true;
+  mind_entry_finite = Decl_kinds.BiFinite;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
   mind_entry_polymorphic = false;
   mind_entry_universes = Univ.UContext.empty;
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
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index edd108071..7ce6bc3e2 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -762,7 +762,7 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
     | Some (projs, pbs) when Array.length projs > 0
-      && mib.Declarations.mind_finite -> 
+      && mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
       let pars = mib.Declarations.mind_nparams in
 	(try 
 	   let l1' = Stack.tail pars sk1 in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 913afb219..4b6107c4e 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -441,7 +441,7 @@ let find_inductive env sigma c =
   let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
   match kind_of_term t with
     | Ind ind
-        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite ->
+        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite ->
         (ind, l)
     | _ -> raise Not_found
 
@@ -449,7 +449,7 @@ let find_coinductive env sigma c =
   let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
   match kind_of_term t with
     | Ind ind
-        when not (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite ->
+        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite ->
         (ind, l)
     | _ -> raise Not_found
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 46f65271f..d5dfd7bf0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -461,7 +461,7 @@ let is_eta_constructor_app env f l1 =
     let mib = lookup_mind (fst ind) env in
       (match mib.Declarations.mind_record with
       | Some (exp,projs) when Array.length projs > 0
-        && mib.Declarations.mind_finite -> 
+        && mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
         Array.length projs == Array.length l1 - mib.Declarations.mind_nparams
       | _ -> false)
   | _ -> false
diff --git a/printing/printer.ml b/printing/printer.ml
index 7938b7bb0..7971e0aaa 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -780,8 +780,15 @@ let print_one_inductive env mib ((_,i) as ind) =
 let print_mutual_inductive env mind mib =
   let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
   in
+  let keyword =
+    let open Decl_kinds in
+    match mib.mind_finite with
+    | Finite -> "Inductive "
+    | BiFinite -> "Variant "
+    | CoFinite -> "CoInductive "
+  in
   hov 0 (pr_polymorphic mib.mind_polymorphic ++
-    str (if mib.mind_finite then "Inductive " else "CoInductive ") ++
+    str keyword ++
     prlist_with_sep (fun () -> fnl () ++ str"  with ")
       (print_one_inductive env mib) inds ++
       pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 7dd59cf05..ffee2e244 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -160,8 +160,14 @@ let print_body is_impl env mp (l,body) =
 	let env = Option.get env in
 	Printer.pr_mutual_inductive_body env (MutInd.make2 mp l) mib
       with e when Errors.noncritical e ->
-	(if mib.mind_finite then str "Inductive " else str "CoInductive")
-	++ name)
+        let keyword =
+          let open Decl_kinds in
+          match mib.mind_finite with
+          | Finite -> "Inductive "
+          | BiFinite -> "Variant "
+          | CoFinite -> "CoInductive "
+        in
+	str keyword ++ name)
 
 let print_struct is_impl env mp struc =
   prlist_with_sep spc (print_body is_impl env mp) struc
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index b81429240..bec80f70d 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -93,7 +93,7 @@ let find_mutually_recursive_statements thms =
           (match kind_of_term t with
           | Ind ((kn,_ as ind), u) when
               let mind = Global.lookup_mind kn in
-              mind.mind_finite && Option.is_empty b ->
+              mind.mind_finite == Decl_kinds.Finite && Option.is_empty b ->
               [ind,x,i],[]
           | _ ->
               error "Decreasing argument is not an inductive assumption.")
@@ -110,7 +110,7 @@ let find_mutually_recursive_statements thms =
           match kind_of_term t with
           | Ind ((kn,_ as ind),u) when
                 let mind = Global.lookup_mind kn in
-                mind.mind_finite && Option.is_empty b ->
+                mind.mind_finite <> Decl_kinds.CoFinite && Option.is_empty b ->
               [ind,x,i]
           | _ ->
               []) 0 (List.rev whnf_hyp_hds)) in
@@ -120,7 +120,7 @@ let find_mutually_recursive_statements thms =
         match kind_of_term whnf_ccl with
         | Ind ((kn,_ as ind),u) when
               let mind = Global.lookup_mind kn in
-              Int.equal mind.mind_ntypes n && not mind.mind_finite ->
+              Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
             [ind,x,0]
         | _ ->
             [] in
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 84fcd6dee..fd871349c 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -48,7 +48,7 @@ let match_with_non_recursive_type t =
         let (hdapp,args) = decompose_app t in
         (match kind_of_term hdapp with
            | Ind (ind,u) ->
-               if not (Global.lookup_mind (fst ind)).mind_finite then
+               if (Global.lookup_mind (fst ind)).mind_finite == Decl_kinds.CoFinite then
 		 Some (hdapp,args)
 	       else
 		 None
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 980f805ef..3da8de072 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -273,9 +273,9 @@ let type_of_string = function
   | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix"
   | "ex" | "scheme" -> Definition
   | "prf" | "thm" -> Lemma
-  | "ind" | "coind" -> Inductive
+  | "ind" | "variant" | "coind" -> Inductive
   | "constr" -> Constructor
-  | "rec" | "corec" -> Record
+  | "indrec" | "rec" | "corec" -> Record
   | "proj" -> Projection
   | "class" -> Class
   | "meth" -> Method
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