diff options
Diffstat (limited to 'tools/coqdoc')
-rw-r--r-- | tools/coqdoc/cpretty.mll | 3 | ||||
-rw-r--r-- | tools/coqdoc/output.ml | 6 |
2 files changed, 5 insertions, 4 deletions
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>" |