diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-04 22:02:51 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-04 22:02:51 +0200 |
| commit | 3a80af7d4d69927af25ed45fa45a6320d8716a80 (patch) | |
| tree | 90b4bdcf294b0b19db55f6b126ea369f71c9bd9b | |
| parent | 31a69c4d0fd7b8325187e8da697a9c283594047d (diff) | |
Recognize "Instance" in coqwc. (Fix for bug #2551)
| -rw-r--r-- | tools/coqwc.mll | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/tools/coqwc.mll b/tools/coqwc.mll index e6655db15..287347282 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -7,7 +7,7 @@ (************************************************************************) (* coqwc - counts the lines of spec, proof and comments in Coq sources - * Copyright (C) 2003 Jean-Christophe Filliâtre *) + * Copyright (C) 2003 Jean-Christophe Filliâtre *) (*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source. It assumes the files to be lexically well-formed. *) @@ -95,6 +95,8 @@ let stars = "(*" '*'* "*)" let dot = '.' (' ' | '\t' | '\n' | '\r' | eof) let proof_start = "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" | "Next" +let def_start = + "Definition" | "Fixpoint" | "Instance" let proof_end = ("Save" | "Qed" | "Defined" | "Abort" | "Admitted") [^'.']* '.' @@ -107,14 +109,10 @@ rule spec = parse | '\n' { newline (); spec lexbuf } | space+ | stars { spec lexbuf } - | proof_start space + | proof_start { seen_spec := true; spec_to_dot lexbuf; proof lexbuf } - | proof_start '\n' - { seen_spec := true; newline (); spec_to_dot lexbuf; proof lexbuf } - | "Program"? "Definition" space + | def_start { seen_spec := true; definition lexbuf } - | "Program"? "Fixpoint" space - { seen_spec := true; definition lexbuf } | character | _ { seen_spec := true; spec lexbuf } | eof { () } @@ -133,7 +131,7 @@ and spec_to_dot = parse { seen_spec := true; spec_to_dot lexbuf } | eof { () } -(*s [definition] scans a definition; passes to [proof] is the body is +(*s [definition] scans a definition; passes to [proof] if the body is absent, and to [spec] otherwise *) and definition = parse |