diff options
| author | Pierre Courtieu | 2019-07-25 08:40:10 +0200 |
|---|---|---|
| committer | GitHub | 2019-07-25 08:40:10 +0200 |
| commit | 6361916d4d80828fd0bcc92c575c59e831b3fa8f (patch) | |
| tree | 3370ac2436dfe5132e2c997706650e4dfca107d0 /coq | |
| parent | 2ada467c2c2964a605659714f2a267db2c915952 (diff) | |
| parent | fa412e1c74cd82dbd15524b44659ca465006f619 (diff) | |
Merge pull request #432 from a0919610611/fix-coqtags
fix coqtags that can't find some theorem and output empty definition
Diffstat (limited to 'coq')
| -rwxr-xr-x | coq/coqtags | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/coq/coqtags b/coq/coqtags index 6a6e5a64..faf6984e 100755 --- a/coq/coqtags +++ b/coq/coqtags @@ -53,7 +53,7 @@ while(<>) # print "----- (",$lp,",",$cp,")\n", $stmt, "\n"; - if($stmt=~/^([ \t]*((Fact)|(Goal)|(Lemma)|(Remark)|(Theorem)|(Proposition)|(Corollary))\s+([\w\']+))\s*:/) + if($stmt=~/^([ \t]*((Fact)|(Goal)|(Lemma)|(Remark)|(Theorem)|(Proposition)|(Corollary))\s+([\w\']+)).*:/) { $tagstring.=$1."\177".$10."\001".$lp.",".$cp."\n"; } elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+[\w\']+)/) @@ -61,7 +61,7 @@ while(<>) elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive)|(CoInductive)|(Record)|(Variant))\s+([\w\']+))/) { - $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; + $tagstring.=$1."\177".$9."\001".$lp.",".$cp."\n"; if($2 eq "Inductive" || $2 eq "CoInductive" || $2 eq "Variant"){ add_constructors($stmt); } |