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.

6 files changed, 7 insertions, 7 deletions

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