Imported Upstream version 8.1~gammaupstream/8.1.gamma

5 files changed, 33 insertions, 23 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 6597c3f6..3647152a 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -6,18 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqdep.ml 8923 2006-06-08 16:39:58Z herbelin $ *)
+(* $Id: coqdep.ml 9276 2006-10-25 13:00:22Z barras $ *)
 
 open Printf
 open Coqdep_lexer
 open Unix
 
-let (/) = Filename.concat
-
-let file_concat l =
-  if l=[] then "<empty>" else
-    List.fold_left (/) (List.hd l) (List.tl l)
-
 let stderr = Pervasives.stderr
 let stdout = Pervasives.stdout
 
@@ -28,12 +22,23 @@ let option_D = ref false
 let option_w = ref false
 let option_i = ref false
 let option_sort = ref false
+let option_slash = ref false
 
 let suffixe = ref ".vo"
 let suffixe_spec = ref ".vi"
 
 type dir = string option
 
+(* filename for printing *)
+let (//) s1 s2 =
+  if !option_slash then s1^"/"^s2 else Filename.concat s1 s2
+
+let (/) = Filename.concat
+
+let file_concat l =
+  if l=[] then "<empty>" else
+    List.fold_left (//) (List.hd l) (List.tl l)
+
 (* Files specified on the command line *)
 let mlAccu  = ref ([] : (string * string * dir) list) 
 and mliAccu = ref ([] : (string * string * dir) list) 
@@ -148,7 +153,7 @@ let cut_prefix p s =
   if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s
 
 let canonize f = match Sys.os_type with
-  | "Win32" -> cut_prefix ".\\" f
+  | "Win32" when not !option_slash -> cut_prefix ".\\" f
   | _ -> cut_prefix "./" f
 
 let sort () = 
@@ -517,6 +522,7 @@ let coqdep () =
       | "-coqlib" :: [] -> usage ()
       | "-suffix" :: (s :: ll) -> suffixe := s ; suffixe_spec := s; parse ll
       | "-suffix" :: [] -> usage ()
+      | "-slash" :: ll -> option_slash := true; parse ll
       | f :: ll -> treat None f; parse ll
       | [] -> ()
   in
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index 597152f5..2c07b9fc 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -50,7 +50,7 @@
 %HEVEA\newcommand{\coqdocindent}[1]{\hspace{#1}\hspace{#1}}
 
 % macro for typesetting the title of a module implementation
-\newcommand{\coqdocmodule}[1]{\section*{Module #1}\markboth{Module #1}{}
+\newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{}
 }
 
 %HEVEA\newcommand{\lnot}{\coqwkw{not}}
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 9b5716ff..5b281b8b 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.mll 8863 2006-05-26 10:33:21Z notin $ i*)
+(*i $Id: index.mll 9204 2006-10-04 13:05:58Z notin $ i*)
 
 {
 
@@ -364,6 +364,7 @@ and end_ident = parse
 and module_ident = parse
   | space+
       { module_ident lexbuf }
+  | '"' { string lexbuf; module_ident lexbuf }
   | ident space* ":="
       { () }
   | ident
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index e6a0a72b..84e03d92 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml 8863 2006-05-26 10:33:21Z notin $ i*)
+(*i $Id: output.ml 9245 2006-10-17 12:53:34Z notin $ i*)
 
 open Cdglobals
 open Index
@@ -118,7 +118,7 @@ module Latex = struct
 
   let header () =
     if !header_trailer then begin
-      printf "\\documentclass[12pt]{article}\n";
+      printf "\\documentclass[12pt]{report}\n";
       if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc;
       printf "\\usepackage[T1]{fontenc}\n";
       printf "\\usepackage{fullpage}\n";
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 5c6c7952..bdb58f86 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretty.mll 8861 2006-05-24 15:52:15Z notin $ i*)
+(*i $Id: pretty.mll 9204 2006-10-04 13:05:58Z notin $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -398,19 +398,22 @@ and coq = parse
       { () }
   | gallina_kw_to_hide
       { let s = lexeme lexbuf in
-	  if !light && section_or_end s then begin 
-	    let eol = skip_to_dot lexbuf in
-	      if eol then coq_bol lexbuf else coq lexbuf 
-	  end else begin
-	    ident s (lexeme_start lexbuf); 
-	    let eol=body lexbuf in 
-	      if eol then coq_bol lexbuf else coq lexbuf
-	  end }
+	  if !light && section_or_end s then 
+	    begin 
+	      let eol = skip_to_dot lexbuf in
+		if eol then coq_bol lexbuf else coq lexbuf 
+	    end 
+	  else 
+	    begin
+	      ident s (lexeme_start lexbuf); 
+	      let eol=body lexbuf in 
+		if eol then coq_bol lexbuf else coq lexbuf
+	    end }
   | gallina_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 }
+	let eol = body lexbuf in
+	  if eol then coq_bol lexbuf else coq lexbuf }
   | space+ { char ' '; coq lexbuf }
   | eof 
       { () }