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, 8 insertions, 2 deletions

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