From b18b40878f071b6c7d67d1a2d031370f7a498d0b Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 3 Sep 2014 11:40:27 +0200
Subject: 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.
---
 interp/dumpglob.ml | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

(limited to 'interp')

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index bf9d2c0b99..87c8cb04d9 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 =
-- 
cgit v1.2.3