Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.

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

3 files changed, 33 insertions, 5 deletions

diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 4e54044473..2e2804cf2b 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -209,6 +209,8 @@ let all_entries () =
 }
 
 (*s Shortcuts for regular expressions. *)
+let digit = ['0'-'9']
+let num = digit+
 
 let space = 
   [' ' '\010' '\013' '\009' '\012']
@@ -225,16 +227,18 @@ let end_hide = "(*" space* "end" space+ "hide" space* "*)"
 (*s Indexing entry point. *)
   
 rule traverse = parse
-  | "Definition" space
+  | ("Program" space+)? "Definition" space
       { current_type := Definition; index_ident lexbuf; traverse lexbuf }
   | "Tactic" space+ "Definition" space
       { current_type := TacticDefinition; index_ident lexbuf; traverse lexbuf }
   | ("Axiom" | "Parameter") space 
       { current_type := Axiom; index_ident lexbuf; traverse lexbuf }
-  | "Fixpoint" space
+  | ("Program" space+)? "Fixpoint" space
       { current_type := Definition; index_ident lexbuf; fixpoint lexbuf;
 	traverse lexbuf }
-  | ("Lemma" | "Theorem") space
+  | ("Program" space+)? ("Lemma" | "Theorem") space
+      { current_type := Lemma; index_ident lexbuf; traverse lexbuf }
+  | "Obligation" space num ("of" ident)?
       { current_type := Lemma; index_ident lexbuf; traverse lexbuf }
   | "Inductive" space
       { current_type := Inductive; 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 8ac25ad269..737cd4d755 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -43,12 +43,15 @@ let is_keyword =
       "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
       "Unset"; "Variable"; "Variables"; 
       "Notation"; 
+      (* Program *)
+      "Program Definition"; "Program Fixpoint"; "Program Lemma";
+      "Obligation"; "Obligations"; "Solve";
       (*i (* correctness *)
       "array"; "assert"; "begin"; "do"; "done"; "else"; "end"; "if";
       "in"; "invariant"; "let"; "of"; "ref"; "state"; "then"; "variant";
       "while"; i*)
-      (*i (* coq terms *)
-      "with"; "Case"; "Cases"; "Prop"; "Set"; "Type"; i*)
+      (*i (* coq terms *) *)
+	"match"; "with"; "end"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="
        ]
 
 (*s Current Coq module *)
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 869df4eef6..80cdb321be 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -257,8 +257,15 @@ let extraction =
   | "Recursive" space+ "Extraction" 
   | "Extract"
 
+
 let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
 
+let prog_kw =
+  "Program" space+ gallina_kw
+  | "Obligation"
+  | "Obligations"
+  | "Solve"
+
 let gallina_kw_to_hide =
   "Implicit"
   | "Ltac"
@@ -344,6 +351,15 @@ rule coq_bol = parse
 	    ident s (lexeme_start lexbuf + nbsp); 
 	    let eol= body lexbuf in
 	      if eol then coq_bol lexbuf else coq lexbuf }
+  | space* prog_kw
+      { let s = lexeme lexbuf in 
+	let nbsp = count_spaces s in
+	  indentation nbsp;
+	  let s = String.sub s nbsp (String.length s - nbsp)  in
+	    ident s (lexeme_start lexbuf + nbsp); 
+	    let eol= body lexbuf in
+	      if eol then coq_bol lexbuf else coq lexbuf }
+
   | space* "(**" space+ "printing" space+ (identifier | token) space+
       { let tok = lexeme lexbuf in
 	let s = printing_token lexbuf in
@@ -414,6 +430,11 @@ and coq = parse
 	  ident s (lexeme_start lexbuf); 
 	let eol = body lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
+  | prog_kw
+      { let s = lexeme lexbuf in 
+	  ident s (lexeme_start lexbuf); 
+	let eol = body lexbuf in
+	  if eol then coq_bol lexbuf else coq lexbuf }
   | space+ { char ' '; coq lexbuf }
   | eof 
       { () }