From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 14 Oct 2010 17:51:11 +0200
Subject: Imported Upstream version 8.3

---
 tools/coqdep_common.ml   | 2 +-
 tools/coqdoc/cpretty.mll | 3 ++-
 tools/coqdoc/output.ml   | 6 +++---
 3 files changed, 6 insertions(+), 5 deletions(-)

(limited to 'tools')

diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index c4e8b23c..0961e398 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -138,7 +138,7 @@ let warning_clash file dir =
       let d2 = Filename.dirname f2 in
       let dl = List.map Filename.dirname (List.rev fl) in
       eprintf
-        "*** Warning: in file %s, \n    required library %s is ambiguous!\n    (found %s.v in "
+        "*** Warning: in file %s, \n    required library %s matches several files in path\n    (found %s.v in "
         file (String.concat "." dir) f;
       List.iter (fun s -> eprintf "%s, " s) dl;
       eprintf "%s and %s; used the latter)\n" d2 d1
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index d24093ff..a23a4f74 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cpretty.mll 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: cpretty.mll 13440 2010-09-19 20:21:12Z herbelin $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -326,6 +326,7 @@ let def_token =
   | "CoInductive"
   | "Equations"
   | "Instance"
+  | "Declare" space+ "Instance"
   | "Global" space+ "Instance"
 
 let decl_token =
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 0b3718ab..cbebbd79 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: output.ml 13541 2010-10-13 19:53:29Z notin $ i*)
 
 open Cdglobals
 open Index
@@ -477,8 +477,6 @@ module Html = struct
 	end
 
   let trailer () =
-    if !index && (get_module false) <> "Index" then
-      printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
     if !header_trailer then
       if !footer_file_spec then
 	let cin = Pervasives.open_in !footer_file in
@@ -490,6 +488,8 @@ module Html = struct
 	  with End_of_file -> Pervasives.close_in cin
       else
 	begin
+	  if !index && (get_module false) <> "Index" then
+	    printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
 	  printf "<hr/>This page has been generated by ";
 	  printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
 	  printf "</div>\n\n</div>\n\n</body>\n</html>"
-- 
cgit v1.2.3