Fix setoid_rewrite documentation examples.

Debug handling of identifiers in coqdoc (should work with modules and
sections) and add missing macros.
Move theories/Program to THEORIESVO to put the files in the standard
library documentation.


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

5 files changed, 42 insertions, 29 deletions

diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index d8cc333367..ca3e08f7fa 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -63,8 +63,8 @@
 }
 
 \usepackage{hyperref}
+\hypersetup{colorlinks=true,linkcolor=black}
 %\usepackage{color}
-%\hypersetup{colorlinks=true,linkcolor=black}
 %\usepackage{multind}
 %\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}}
 
@@ -79,7 +79,10 @@
 \newcommand{\coqdefinition}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
 \newcommand{\coqdefinitionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
 
-\newcommand{\coqvariable}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
+%\newcommand{\coqvariable}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
+%\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
+\newcommand{\coqvariable}[2]{\coqdocid{#2}}
+\newcommand{\coqaxiom}[2]{\coqdocid{#2}}
 
 \newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
 \newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}}
@@ -108,6 +111,8 @@
 \newcommand{\coqprojection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
 \newcommand{\coqprojectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
 
+\newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}}
+
 %HEVEA\newcommand{\lnot}{\coqwkw{not}}
 %HEVEA\newcommand{\lor}{\coqwkw{or}}
 %HEVEA\newcommand{\land}{\&}
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 9f0c3d24a9..ec04017c44 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -60,6 +60,8 @@ type 'a index = {
   idx_entries : (char * (string * 'a) list) list;
   idx_size : int }
 
+val current_library : string ref
+
 val all_entries : unit -> 
       (coq_module * entry_type) index *
       (entry_type * coq_module index) list
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index fa619a9434..1fa7c2498b 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -44,16 +44,20 @@ type index_entry =
 
 let current_type = ref Library
 let current_library = ref ""
-  (** referes to the file being parsed *)
+  (** refers to the file being parsed *)
 
 let table = Hashtbl.create 97
   (** [table] is used to store references and definitions *)
 
-let add_def loc ty id = Hashtbl.add table (!current_library, loc) (Def (id, ty))
-
-let add_ref m loc m' id ty = 
-  Hashtbl.add table (m, loc) (Ref (m', id, ty))
+let full_ident sp id =
+  if sp <> "<>" then sp ^ "." ^ id else id
+    
+let add_def loc ty sp id = 
+  Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty))
 
+let add_ref m loc m' sp id ty = 
+  Hashtbl.add table (m, loc) (Ref (m', full_ident sp id, ty))
+    
 let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id))
 
 let find m l = Hashtbl.find table (m, l)
@@ -288,7 +292,7 @@ and index_ident = parse
 	      | Lemma -> make_fullid id
 	      | _ -> id 
 	in 
-	  add_def (lexeme_start lexbuf) !current_type fullid }
+	  add_def (lexeme_start lexbuf) !current_type "" fullid }
   | eof    
       { () }
   | _      
@@ -300,7 +304,7 @@ and index_idents = parse
   | space+ | ','
       { index_idents lexbuf }
   | ident  
-      { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf);
+      { add_def (lexeme_start lexbuf) !current_type "" (lexeme lexbuf);
 	index_idents lexbuf }
   | eof    
       { () }
@@ -380,7 +384,7 @@ and module_ident = parse
       { () }
   | ident
       { let id = lexeme lexbuf in
-	  begin_module id; add_def (lexeme_start lexbuf) !current_type id }
+	  begin_module id; add_def (lexeme_start lexbuf) !current_type "" id }
   | eof
       { () }
   | _
@@ -439,13 +443,13 @@ and module_refs = parse
 		current_library := !cur_mod
 	    | 'R' ->
 		(try
-		    Scanf.sscanf s "R%d %s %s %s"
-		      (fun loc lib_dp full_id ty ->
-			add_ref !cur_mod loc lib_dp full_id (type_of_string ty))
+		    Scanf.sscanf s "R%d %s %s %s %s"
+		      (fun loc lib_dp sp id ty ->
+			add_ref !cur_mod loc lib_dp sp id (type_of_string ty))
 		  with _ -> ())
 	    | _ -> 
-		try Scanf.sscanf s "%s %d %s"
-		  (fun ty loc id -> add_def loc (type_of_string ty) id)
+		try Scanf.sscanf s "%s %d %s %s"
+		  (fun ty loc sp id -> add_def loc (type_of_string ty) sp id)
 		with Scanf.Scan_failure _ -> ()
 	end
       done; assert false
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 251fb23571..5b68e94cca 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -36,7 +36,7 @@ let is_keyword =
       "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example"; 
       "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
       "Hypothesis"; "Hypotheses"; 
-      "Immediate"; "Implicit"; "Import"; "Inductive"; 
+      "Resolve"; "Unfold"; "Immediate"; "Implicit"; "Import"; "Inductive"; 
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; 
       "Module"; "Module Type"; "Declare Module"; "Include";
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
@@ -46,18 +46,15 @@ let is_keyword =
       "Notation"; "Reserved Notation"; "Tactic Notation";
       "Delimit"; "Bind"; "Open"; "Scope";
       "Boxed"; "Unboxed";
-      "Arguments";
-      "Instance"; "Class"; "Instantiation";
+      "Arguments"; 
+      "Typeclasses"; "Instance"; "Class"; "Instantiation";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
       "Program Instance";
-      (*i (* correctness *)
-      "array"; "assert"; "begin"; "do"; "done"; "else"; "end"; "if";
-      "in"; "invariant"; "let"; "of"; "ref"; "state"; "then"; "variant";
-      "while"; i*)
       (*i (* coq terms *) *)
-	"match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="
+	"match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; 
+	"if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"
        ]
 
 let is_tactic = 
@@ -65,9 +62,12 @@ let is_tactic =
     [ "intro"; "intros"; "apply"; "rewrite"; "setoid_rewrite";
       "destruct"; "induction"; "elim"; "dependent"; 
       "generalize"; "clear"; "rename"; "move"; "set"; "assert";
-      "cut"; "assumption"; "exact";
-      "unfold"; "red"; "compute"; "at"; "in"; "by";
-      "reflexivity"; "symmetry"; "transitivity" ]
+      "cut"; "assumption"; "exact"; "split"; "try"; "discriminate";
+      "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by";
+      "reflexivity"; "symmetry"; "transitivity";
+      "replace"; "setoid_replace"; "inversion"; "pattern";
+      "trivial"; "exact"; "tauto"; "firstorder"; "ring";
+      "clapply"; "program_simpl"; "eapply"; "auto"; "eauto" ]
 
 (*s Current Coq module *)
 
@@ -94,6 +94,7 @@ let remove_printing_token = Hashtbl.remove token_pp
 let _ = List.iter 
 	  (fun (s,l) -> Hashtbl.add token_pp s (Some l, None))
 	  [ "*" ,  "\\ensuremath{\\times}";
+	    "|", "\\ensuremath{|}";
 	    "->",  "\\ensuremath{\\rightarrow}";
 	    "->~",  "\\ensuremath{\\rightarrow\\lnot}";
 	    "->~~",  "\\ensuremath{\\rightarrow\\lnot\\lnot}";
@@ -246,8 +247,6 @@ module Latex = struct
   let ident s loc = 
     if is_keyword s then begin
       printf "\\coqdockw{"; raw_ident s; printf "}"
-    end else if is_tactic s then begin
-      printf "\\coqdoctac{"; raw_ident s; printf "}"
     end else begin
       begin
 	try
@@ -261,7 +260,9 @@ module Latex = struct
 	     | Mod _ ->
 		 printf "\\coqdocid{"; raw_ident s; printf "}")
 	with Not_found ->
-	  printf "\\coqdocvar{"; raw_ident s; printf "}"
+	  if is_tactic s then begin
+	    printf "\\coqdoctac{"; raw_ident s; printf "}"
+	  end else begin printf "\\coqdocvar{"; raw_ident s; printf "}" end
       end
     end
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 2e0f46795a..a9ad92f4c7 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -661,6 +661,7 @@ and printing_token_body = parse
 
   let coq_file f m =
     reset ();
+    Index.current_library := m;
     Output.start_module ();
     let c = open_in f in
     let lb = from_channel c in