From fa412e1c74cd82dbd15524b44659ca465006f619 Mon Sep 17 00:00:00 2001
From: Yu-Fu Fu
Date: Thu, 25 Jul 2019 10:39:01 +0800
Subject: fix coqtags that can't find some theorem and output empty definition
 name

---
 coq/coqtags | 4 ++--
 1 file 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);
 	}
-- 
cgit v1.2.3