Add Program keywords to coqwc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9691 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 2 deletions

diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index 35004f79d..9c0019342 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -97,7 +97,7 @@ let rcs = "\036" rcs_keyword [^ '$']* "\036"
 let stars = "(*" '*'* "*)"
 let dot = '.' (' ' | '\t' | '\n' | '\r' | eof)
 let proof_start =   
-  "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness"
+  "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" | "Next"
 let proof_end =
   ("Save" | "Qed" | "Defined" | "Abort" | "Admitted") [^'.']* '.'
 
@@ -114,8 +114,10 @@ rule spec = parse
            { seen_spec := true; spec_to_dot lexbuf; proof lexbuf }
   | proof_start '\n'
            { seen_spec := true; newline (); spec_to_dot lexbuf; proof lexbuf }
-  | "Definition" space
+  | "Program"? "Definition" space
            { seen_spec := true; definition lexbuf }
+  | "Program"? "Fixpoint" space
+  	   { seen_spec := true; definition lexbuf }
   | character | _ 
 	   { seen_spec := true; spec lexbuf }
   | eof    { () }