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.

1 files changed, 1 insertions, 1 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 6f0ead941e..94239d0bf3 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;