diff options
| author | Maxime Dénès | 2017-10-03 15:34:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-03 15:34:29 +0200 |
| commit | 3a8209d262ef586baee5b76161afd83893d1dad3 (patch) | |
| tree | 5e4c3b91f81989e42c491ee9a56fd6ff2844f97e | |
| parent | 01050348ca54a3ac42da954d85b19c331d0c11db (diff) | |
| parent | d6188188c444a95e3d40c3926274b7e526e96b82 (diff) | |
Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start proof for coqwc
| -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 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 = |