diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
| commit | 3e96002677226c0cdaa8f355938a76cfb37a722a (patch) | |
| tree | 3ca96e142fdb68e464d2f5f403f315282b94f922 /tools | |
| parent | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff) | |
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdep_common.ml | 2 | ||||
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 3 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 6 |
3 files changed, 6 insertions, 5 deletions
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>" |