From ac2fdfb222083faa9c3893194e020bed38555ddb Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 2 Sep 2014 18:02:26 +0200
Subject: Add a [Variant] declaration which allows to write non-recursive
 variant types.

Just like the [Record] keyword allows only non-recursive records.
---
 printing/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index dce073becb..514017d454 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -652,7 +652,7 @@ let rec pr_vernac = function
         let (_,_,_,k,_),_ = List.hd l in
 	match k with Record -> "Record" | Structure -> "Structure"
 	  | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
-	  | Class _ -> "Class" in
+	  | Class _ -> "Class" | Variant -> "Variant" in
       hov 1 (pr_oneind key (List.hd l)) ++
       (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
 
-- 
cgit v1.2.3