diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-04 16:04:10 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-04 16:04:10 +0200 |
| commit | 5b688868704cc1097aded2caea27d89047318eb1 (patch) | |
| tree | c66dc6808a471951f8af95d3b1b1fb4739494c88 | |
| parent | b8e76c36b0fd4016c4d5b4098a11dc733872ff5f (diff) | |
Support other forms of "Proof" in coqwc. (Fix for bug #2735)
| -rw-r--r-- | tools/coqwc.mll | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/coqwc.mll b/tools/coqwc.mll index 50f989e7c..e6655db15 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -159,6 +159,8 @@ and proof = parse { proof lexbuf } | '\n' { newline (); proof lexbuf } | "Proof" space* '.' + | "Proof" space+ "with" + | "Proof" space+ "using" { seen_proof := true; proof lexbuf } | "Proof" space { proof_term lexbuf } |