aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coqtags
diff options
context:
space:
mode:
Diffstat (limited to 'coq/coqtags')
-rwxr-xr-xcoq/coqtags4
1 files changed, 2 insertions, 2 deletions
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"){