diff options
| author |  Tej Chajed <tchajed@mit.edu> | 2018-08-17 11:50:57 -0400 |
|---|---|---|
| committer | Tej Chajed <tchajed@mit.edu> | 2018-08-17 11:50:57 -0400 |
| commit | 5c27e4a9398cb366e087594dd1c72e4c084fae01 (patch) | |
| tree | cf24865ec0299070cf7d24af6a81cec9e0df98a7 /coq/coqtags | |
| parent | b7f17b7ca09276be5cd29263bd5574fdd6fa4d2c (diff) | |
Support the Variant vernacular
Syntactically looks much like an Inductive, though it is non-recursive
so "where" (mutual recursion) is not supported.
Diffstat (limited to 'coq/coqtags')
| -rwxr-xr-x | coq/coqtags | 4 |
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"){ |