From 5c27e4a9398cb366e087594dd1c72e4c084fae01 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Fri, 17 Aug 2018 11:50:57 -0400
Subject: Support the Variant vernacular

Syntactically looks much like an Inductive, though it is non-recursive
so "where" (mutual recursion) is not supported.
---
 coq/coqtags | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'coq/coqtags')

diff --git a/coq/coqtags b/coq/coqtags
index 50d4a2f5..6a6e5a64 100755
--- a/coq/coqtags
+++ b/coq/coqtags
@@ -59,10 +59,10 @@ while(<>)
     elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+[\w\']+)/)
       { adddecs($stmt,$1); }
 
-    elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive)|(CoInductive)|(Record))\s+([\w\']+))/)
+    elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive)|(CoInductive)|(Record)|(Variant))\s+([\w\']+))/)
     {
 	$tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n";
-	if($2 eq "Inductive" || $2 eq "CoInductive"){
+	if($2 eq "Inductive" || $2 eq "CoInductive" || $2 eq "Variant"){
 	    add_constructors($stmt);
 	}
 	elsif($2 eq "Record"){
-- 
cgit v1.2.3