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.
---
 tools/coqdoc/index.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tools')

diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 980f805efe..3da8de0721 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
-- 
cgit v1.2.3