Add a [Variant] declaration which allows to write non-recursive variant types.

Just like the [Record] keyword allows only non-recursive records.

7 files changed, 12 insertions, 3 deletions

diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index ae39a1249..9a6135301 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -92,6 +92,7 @@ let commands = [
    ];
   ["Read Module";
    "Record";
+   "Variant";
    "Remark";
    "Remove LoadPath";
    "Remove Printing Constructor";
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 238eeb82e..7f3417443 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -176,7 +176,7 @@ type local_decl_expr =
   | AssumExpr of lname * constr_expr
   | DefExpr of lname * constr_expr * constr_expr option
 
-type inductive_kind = Inductive_kw | CoInductive | Record | Structure | Class of bool (* true = definitional, false = inductive *)
+type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *)
 type decl_notation = lstring * constr_expr * scope_name option
 type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 013381382..3437256ed 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -269,7 +269,8 @@ GEXTEND Gram
   ;
   finite_token:
     [ [ "Inductive" -> (Inductive_kw,Finite)
-      | "CoInductive" -> (CoInductive,CoFinite) ] ]
+      | "CoInductive" -> (CoInductive,CoFinite)
+      | "Variant" -> (Variant,BiFinite) ] ]
   ;
   infer_token:
     [ [ IDENT "Infer" -> true | -> false ] ]
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index dce073bec..514017d45 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))
 
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 73c313252..d6eb68882 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 28480d4bd..0561d9a08 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";
diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el
index cbf4433be..c25abece1 100644
--- a/tools/gallina-syntax.el
+++ b/tools/gallina-syntax.el
@@ -360,6 +360,11 @@
     ("Inductive (3 args)" "indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." t )
     ("Inductive (4 args)" "indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t )
     ("Inductive (5 args)" "indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t )
+    ("Variant" "indv" "Variant # : # := # : #." t "Variant")
+    ("Variant (2 args)" "indv2" "Variant # : # :=\n| # : #\n| # : #." t )
+    ("Variant (3 args)" "indv3" "Variant # : # :=\n| # : #\n| # : #\n| # : #." t )
+    ("Variant (4 args)" "indv4" "Variant # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t )
+    ("Variant (5 args)" "indv5" "Variant # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t )
     ("Let" "Let" "Let # : # := #." t "Let")
     ("Ltac" "ltac" "Ltac # := #" t "Ltac")
     ("Module :=" "mo" "Module # : # := #." t ) ; careful