aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coqtags
diff options
context:
space:
mode:
authorGravatar Hendrik Tews <hendrik@askra.de>2017-01-17 15:55:13 +0100
committerGravatar Hendrik Tews <hendrik@askra.de>2017-01-17 16:58:01 +0100
commit94439d50451ad4a3e14c705dc2774c76e6530074 (patch)
tree97a7b2a2478e607d860e503849a6e05cfd9623ec /coq/coqtags
parentf487c716306913b2a02cde1bcfdcc12b81137c14 (diff)
fix coqtags
@psteckler I believe you have this patch already in your branch.
Diffstat (limited to 'coq/coqtags')
-rwxr-xr-xcoq/coqtags2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coqtags b/coq/coqtags
index 6d874e9d..76b5bcc9 100755
--- a/coq/coqtags
+++ b/coq/coqtags
@@ -52,7 +52,7 @@ while(<>)
{ $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; }
elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+[\w\']+)/)
- { do adddecs($stmt,$1) }
+ { adddecs($stmt,$1); }
elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+[\w\']+)/)
{ $tagstring.=$1."\177".$6."\001".$lp.",".$cp."\n"; }