From d6188188c444a95e3d40c3926274b7e526e96b82 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Tue, 26 Sep 2017 15:23:37 -0400
Subject: look for Obligation num or Next Obligation to start proof

---
 tools/coqwc.mll | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index a0b6bfbbed..6ddeeb9b28 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -94,7 +94,7 @@ let rcs = "\036" rcs_keyword [^ '$']* "\036"
 let stars = "(*" '*'* "*)"
 let dot = '.' (' ' | '\t' | '\n' | '\r' | eof)
 let proof_start =
-  "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" | "Next"
+  "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" space+ (['0' - '9'])+ | "Next" space+ "Obligation"
 let def_start =
   "Definition" | "Fixpoint" | "Instance"
 let proof_end =
-- 
cgit v1.2.3