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.
---
 tools/coqdoc/cpretty.mll | 1 +
 tools/coqdoc/output.ml   | 1 +
 2 files changed, 2 insertions(+)

(limited to 'tools/coqdoc')

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 73c313252f..d6eb68882a 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -313,6 +313,7 @@ let def_token =
   | "Boxed"
   | "CoFixpoint"
   | "Record"
+  | "Variant"
   | "Structure"
   | "Scheme"
   | "Inductive"
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 28480d4bd4..0561d9a081 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -50,6 +50,7 @@ let is_keyword =
       "subgoal"; "subgoals"; "vm_compute";
       "Opaque"; "Transparent"; "Time";
       "Extraction"; "Extract";
+      "Variant";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
-- 
cgit v1.2.3