Enhancements to coqdoc, better globalization of sections and modules.

Minor fix in Morphisms which prevented working with higher-order
morphisms and PER relations.


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

4 files changed, 62 insertions, 21 deletions

diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index ca3e08f7fa..ca454d852b 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -44,6 +44,13 @@
 % macro for typesetting constant identifiers
 \newcommand{\coqdoccst}[1]{\textsf{#1}}
 
+% macro for typesetting module identifiers
+\newcommand{\coqdocmod}[1]{\textsc{\textsf{#1}}}
+
+% macro for typesetting module constant identifiers (e.g. Parameters in
+% module types)
+\newcommand{\coqdocax}[1]{\textsl{\textsf{#1}}}
+
 % macro for typesetting inductive type identifiers
 \newcommand{\coqdocind}[1]{\textbf{\textsf{#1}}}
 
@@ -62,13 +69,15 @@
 \newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{}
 }
 
-\usepackage{hyperref}
-\hypersetup{colorlinks=true,linkcolor=black}
+\usepackage[pdftex]{hyperref}
+\hypersetup{raiselinks=true,colorlinks=true,linkcolor=black}
+\usepackage[all]{hypcap}
+\usepackage{xr}
 %\usepackage{color}
 %\usepackage{multind}
 %\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}}
 
-\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{#3}}
+\newcommand{\coqdef}[3]{\phantomsection\hypertarget{coq:#1}{#3}}
 \newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}}
 
 \newcommand{\coqdocvar}[1]{{\textit{#1}}}
@@ -82,7 +91,6 @@
 %\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}}}
@@ -113,6 +121,25 @@
 
 \newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}}
 
+\newcommand{\coqsection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqsectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+%\newcommand{\coqlibrary}[2]{\chapter{Library \coqdoccst{#2}}\label{coq:#1}}
+  
+%\newcommand{\coqlibraryref}[2]{\ref{coq:#1}}
+
+\newcommand{\coqlibrary}[2]{\cleardoublepage\phantomsection
+  \hypertarget{coq:#1}{\chapter{Library \coqdoccst{#2}}}}
+  
+\newcommand{\coqlibraryref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocax{#2}}}
+\newcommand{\coqaxiomref}[2]{\coqref{#1}{\coqdocax{#2}}}
+
+\newcommand{\coqmodule}[2]{\coqdef{#1}{#2}{\coqdocmod{#2}}}
+\newcommand{\coqmoduleref}[2]{\coqref{#1}{\coqdocmod{#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 ec04017c44..9831ca3cb0 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -29,6 +29,7 @@ type entry_type =
   | TacticDefinition
   | Abbreviation
   | Notation
+  | Section
 
 val type_name : entry_type -> string
 
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 1fa7c2498b..ab23f2210a 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -36,6 +36,7 @@ type entry_type =
   | TacticDefinition
   | Abbreviation
   | Notation
+  | Section
 
 type index_entry = 
   | Def of string * entry_type
@@ -50,7 +51,13 @@ let table = Hashtbl.create 97
   (** [table] is used to store references and definitions *)
 
 let full_ident sp id =
-  if sp <> "<>" then sp ^ "." ^ id else id
+  if sp <> "<>" then 
+    if id <> "<>" then 
+      sp ^ "." ^ id 
+    else sp 
+  else if id <> "<>" 
+  then id 
+  else ""
     
 let add_def loc ty sp id = 
   Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty))
@@ -195,7 +202,8 @@ let type_name = function
   | TacticDefinition -> "tactic"
   | Abbreviation -> "abbreviation"
   | Notation -> "notation"
-      
+  | Section -> "section"
+
 let all_entries () =
   let gl = ref [] in
   let add_g s m t = gl := (s,(m,t)) :: !gl in
@@ -421,14 +429,15 @@ and module_refs = parse
     | "meth" -> Method
     | "inst" -> Instance
     | "var" -> Variable
-    | "ax" -> Axiom
+    | "defax" | "prfax" | "ax" -> Axiom
     | "syndef" -> Abbreviation
     | "not" -> Notation
+    | "lib" -> Library
+    | "mod" | "modtype" -> Module
+    | "tac" -> TacticDefinition
+    | "sec" -> Section
     | s -> raise (Invalid_argument ("type_of_string:" ^ s))
-(*   | Library *)
-(*   | Module *)
-(*   | TacticDefinition *)
-
+	
   let read_glob f = 
     let c = open_in f in
     let cur_mod = ref "" in
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 5b68e94cca..009e4dd11a 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -36,17 +36,17 @@ let is_keyword =
       "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example"; 
       "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
       "Hypothesis"; "Hypotheses"; 
-      "Resolve"; "Unfold"; "Immediate"; "Implicit"; "Import"; "Inductive"; 
+      "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive"; 
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; 
       "Module"; "Module Type"; "Declare Module"; "Include";
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
-      "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
+      "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
       "Set"; "Unset"; "Variable"; "Variables"; 
       "Notation"; "Reserved Notation"; "Tactic Notation";
-      "Delimit"; "Bind"; "Open"; "Scope";
-      "Boxed"; "Unboxed";
-      "Arguments"; 
+      "Delimit"; "Bind"; "Open"; "Scope"; 
+      "Boxed"; "Unboxed"; "Inline";
+      "Arguments"; "Add"; "Strict";
       "Typeclasses"; "Instance"; "Class"; "Instantiation";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
@@ -65,7 +65,8 @@ let is_tactic =
       "cut"; "assumption"; "exact"; "split"; "try"; "discriminate";
       "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by";
       "reflexivity"; "symmetry"; "transitivity";
-      "replace"; "setoid_replace"; "inversion"; "pattern";
+      "replace"; "setoid_replace"; "inversion"; "inversion_clear";
+      "pattern"; "intuition"; "congruence";
       "trivial"; "exact"; "tauto"; "firstorder"; "ring";
       "clapply"; "program_simpl"; "eapply"; "auto"; "eauto" ]
 
@@ -190,7 +191,9 @@ module Latex = struct
 
   let start_module () = 
     if not !short then begin
-      printf "\\coqdocmodule{"; 
+      printf "\\coqlibrary{"; 
+      label_ident !current_module; 
+      printf "}{";
       raw_ident !current_module; 
       printf "}\n\n"
     end
@@ -231,13 +234,14 @@ module Latex = struct
 	raw_ident s
     i*)
 
-  let ident_ref m fid typ s = 
+  let ident_ref m fid typ s =
+    let id = if fid <> "" then (m ^ "." ^ fid) else m in
     match find_module m with
       | Local ->
-	  printf "\\coq%sref{" (type_name typ); label_ident (m ^ "." ^ fid); printf "}{"; raw_ident s; printf "}"
+	  printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
       | Coqlib when !externals ->
 	  let _m = Filename.concat !coqlib m in
-	    printf "\\coq%sref{" (type_name typ); label_ident (m ^ "." ^ fid); printf "}{"; raw_ident s; printf "}"
+	    printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
       | Coqlib | Unknown ->
 	  raw_ident s