diff options
| author |  Paul Steckler <steck@stecksoft.com> | 2017-09-26 15:23:37 -0400 |
|---|---|---|
| committer | Paul Steckler <steck@stecksoft.com> | 2017-09-26 15:23:37 -0400 |
| commit | d6188188c444a95e3d40c3926274b7e526e96b82 (patch) | |
| tree | 22407baec93eef1913933a38bbb3d86b99be0e05 /tools | |
| parent | 4b6383889d4d38de4c9a28bee960b30114a51b16 (diff) | |
look for Obligation num or Next Obligation to start proof
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqwc.mll | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqwc.mll b/tools/coqwc.mll index a0b6bfbbe..6ddeeb9b2 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 = |