Use the standalone coq2html tool to generate the HTML documentation

coq2html is now a standalone project (https://github.com/xavierleroy/coq2html)
packaged as coq-coq2html in OPAM-Coq.

5 files changed, 115 insertions, 752 deletions

diff --git a/doc/coq2html.css b/doc/coq2html.css
deleted file mode 100644
index c5627bfb..00000000
--- a/doc/coq2html.css
+++ /dev/null
@@ -1,97 +0,0 @@
-/* Classes:
-     h1.title     the title of the page
-     div.coq      encloses all generated body
-     div.doc      contents of (** *) comments
-     div.footer   footer
-     div.togglescript   "Proof." line
-     div.proofscript  contents of proof script
-     span.docright contents of (**r *) comments
-     span.bracket contents of [ ] within comments
-     span.comment contents of (* *) comments
-     span.kwd     Coq keyword
-     span.tactic  Coq tactic
-     span.id      any other identifier
-*/
-
-body {
-  color: black;
-  background: white;
-}
-
-h1.title {
-  font-size: 2em;
-  text-align: center
-}
-
-h1 {
-  font-size: 1.5em;
-}
-h2 {
-  font-size: 1.17em;
-}
-h3 {
-  font-size: 1em;
-}
-
-h1, h2, h3 {
-  font-family: sans-serif;
-  margin-left: -5%;
-}
-
-div.coq {
-  margin-left: 15%;
-  margin-right: 5%;
-  font-family: monospace;
-}
-
-div.doc {
-  margin-left: -5%;
-  margin-top: 0.2em;
-  margin-bottom: 0.5em;
-  font-family: serif;
-}
-
-div.toggleproof {
-  font-size: 0.8em;
-  text-decoration: underline;
-}
-
-div.toggleproof:hover {
-  cursor: pointer;
-}
-
-div.proofscript {
-  font-size: 0.8em;
-}
-
-div.footer {
-  margin-top: 1em;
-  margin-bottom: 1em;
-  font-size: 0.8em;
-  font-style: italic;
-}  
-
-span.docright {
-  position: absolute;
-  left: 60%;
-  width: 40%;
-  font-family: serif;
-}
-
-span.bracket {
-  font-family: monospace;
-  color: #008000;
-}
-
-span.kwd {
-  color:  #cf1d1d;
-}
-
-span.comment {
-  color:  #008000;
-}
-
-a:visited {color : #416DFF; text-decoration : none; }
-a:link {color : #416DFF; text-decoration : none; }
-a:hover {text-decoration : none; }
-a:active {text-decoration : none; }
diff --git a/doc/coq2html.js b/doc/coq2html.js
deleted file mode 100644
index a840b004..00000000
--- a/doc/coq2html.js
+++ /dev/null
@@ -1,24 +0,0 @@
-function toggleDisplay(id)
-{
-   var elt = document.getElementById(id);
-   if (elt.style.display == 'none') {
-     elt.style.display = 'block';
-   } else {
-     elt.style.display = 'none';
-   }
-}
-
-function hideAll(cls)
-{
-  var testClass = new RegExp("(^|s)" + cls + "(s|$)");
-  var tag = tag || "*";
-  var elements = document.getElementsByTagName("div");
-  var current;
-  var length = elements.length;
-  for(var i=0; i<length; i++){
-    current = elements[i];
-    if(testClass.test(current.className)) {
-      current.style.display = 'none';
-    }
-  }
-}
diff --git a/doc/coq2html.mll b/doc/coq2html.mll
deleted file mode 100644
index cdc844dc..00000000
--- a/doc/coq2html.mll
+++ /dev/null
@@ -1,454 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-{
-open Printf
-
-(** Cross-referencing *)
-
-let current_module = ref ""
-
-type xref =
-  | Def of string * string    (* path, type *)
-  | Ref of string * string * string (* unit, path, type *)
-
-let xref_table : (string * int, xref) Hashtbl.t = Hashtbl.create 273
-let xref_modules : (string, unit) Hashtbl.t = Hashtbl.create 29
-
-let path sp id =
-  match sp, id with
-  | "<>", "<>" -> ""
-  | "<>", _    -> id
-  | _   , "<>" -> sp
-  | _   , _    -> sp ^ "." ^ id
-
-let add_module m =
-  (*eprintf "add_module %s\n" m;*)
-  Hashtbl.add xref_modules m ()
-
-let add_reference curmod pos dp sp id ty =
-  (*eprintf "add_reference %s %d %s %s %s %s\n" curmod pos dp sp id ty;*)
-  if not (Hashtbl.mem xref_table (curmod, pos))
-  then Hashtbl.add xref_table (curmod, pos) (Ref(dp, path sp id, ty))
-
-let add_definition curmod pos sp id ty =
-  if not (Hashtbl.mem xref_table (curmod, pos))
-  then Hashtbl.add xref_table (curmod, pos) (Def(path sp id, ty))
-
-type link = Link of string | Anchor of string | Nolink
-
-let coqlib_url = "http://coq.inria.fr/library/"
-
-let re_coqlib = Str.regexp "Coq\\."
-let re_sane_path = Str.regexp "[A-Za-z0-9_.]+$"
-let re_shortname = Str.regexp "^.*\\."
-
-let shortname m = Str.replace_first re_shortname "" m
-
-let crossref m pos =
-  (*eprintf "crossref %s %d\n" m pos;*)
-  try match Hashtbl.find xref_table (m, pos) with
-  | Def(p, _) ->
-      Anchor p
-  | Ref(m', p, _) ->
-      let url =
-        if Hashtbl.mem xref_modules m' then
-          shortname m' ^ ".html"
-        else if Str.string_match re_coqlib m' 0 then
-          coqlib_url ^ m' ^ ".html"
-        else
-          raise Not_found in
-      if p = "" then
-        Link url
-      else if Str.string_match re_sane_path p 0 then
-        Link(url ^ "#" ^ p)
-      else
-        Nolink
-  with Not_found ->
-    Nolink
-
-(** Keywords, etc *)
-
-module StringSet = Set.Make(String)
-
-let mkset l = List.fold_right StringSet.add l StringSet.empty
-
-let coq_keywords = mkset [
-  "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let";
-  "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":=";
-  "where"; "struct"; "wf"; "measure";
-  "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check";
-  "Coercion"; "CoFixpoint"; "CoInductive"; "Corollary"; "Defined";
-  "Definition"; "End"; "Eval"; "Example"; "Export"; "Fact"; "Fix";
-  "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis";
-  "Hypotheses"; "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"; "Induction"; "for"; "Sort"; "Section"; "Show";
-  "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; "Set";
-  "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
-  "Notation"; "Reserved"; "Tactic"; "Delimit"; "Bind"; "Open";
-  "Scope"; "Boxed"; "Unboxed"; "Inline"; "Implicit Arguments"; "Add";
-  "Strict"; "Typeclasses"; "Instance"; "Global Instance"; "Class";
-  "Instantiation"; "subgoal"; "Program"; "Example"; "Obligation";
-  "Obligations"; "Solve"; "using"; "Next"; "Instance"; "Equations";
-  "Equations_nocomp"
-]
-
-let coq_tactics = mkset [
-  "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear";
-  "injection"; "elimtype"; "progress"; "setoid_rewrite"; "destruct";
-  "destruction"; "destruct_call"; "dependent"; "elim";
-  "extensionality"; "f_equal"; "generalize"; "generalize_eqs";
-  "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
-  "set"; "assert"; "do"; "repeat"; "cut"; "assumption"; "exact";
-  "split"; "subst"; "try"; "discriminate"; "simpl"; "unfold"; "red";
-  "compute"; "at"; "in"; "by"; "reflexivity"; "symmetry";
-  "transitivity"; "replace"; "setoid_replace"; "inversion";
-  "inversion_clear"; "pattern"; "intuition"; "congruence"; "fail";
-  "fresh"; "trivial"; "exact"; "tauto"; "firstorder"; "ring";
-  "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto";
-  "eauto"
-]
-
-(** HTML generation *)
-
-let oc = ref stdout
-
-let character = function
-  | '<' -> output_string !oc "&lt;"
-  | '>' -> output_string !oc "&gt;"
-  | '&' -> output_string !oc "&amp;"
-  |  c  -> output_char !oc c
-
-let section_level = function
-  | "*" -> 1
-  | "**" -> 2
-  | _ -> 3
-
-let start_section sect =
-  fprintf !oc "<h%d>" (section_level sect)
-let end_section sect =
-  fprintf !oc "</h%d>\n" (section_level sect)
-
-let start_doc_right () =
-  fprintf !oc "<span class=\"docright\">(* "
-let end_doc_right () =
-  fprintf !oc " *)</span>"
-
-let enum_depth = ref 0
-
-let  set_enum_depth d =
-  if !enum_depth < d then begin
-    fprintf !oc "<ul>\n";
-    fprintf !oc "<li>\n";
-    incr enum_depth;
-  end
-  else if !enum_depth > d then begin
-    fprintf !oc "</li>\n";
-    fprintf !oc "</ul>\n";
-    decr enum_depth;
-  end
-  else if !enum_depth > 0 then begin
-    fprintf !oc "</li>\n";
-    fprintf !oc "<li>\n"
-  end
-
-let start_doc () =
-  fprintf !oc "<div class=\"doc\">"
-let end_doc () =
-  set_enum_depth 0;
-  fprintf !oc "</div>\n"
-
-let ident pos id =
-  if StringSet.mem id coq_keywords then
-    fprintf !oc "<span class=\"kwd\">%s</span>" id
-  else if StringSet.mem id coq_tactics then
-    fprintf !oc "<span class=\"tactic\">%s</span>" id
-  else match crossref !current_module pos with
-  | Nolink ->
-      fprintf !oc "<span class=\"id\">%s</span>" id
-  | Link p ->
-      fprintf !oc "<span class=\"id\"><a href=\"%s\">%s</a></span>" p id
-  | Anchor p ->
-      fprintf !oc "<span class=\"id\"><a name=\"%s\">%s</a></span>" p id
-
-let space s =
-  for _ = 1 to String.length s do fprintf !oc "&nbsp;" done
-
-let newline () =
-  fprintf !oc "<br/>\n"
-
-let dashes = function
-  | "-" -> set_enum_depth 1
-  | "--" -> set_enum_depth 2
-  | "---" -> set_enum_depth 3
-  | "----" -> set_enum_depth 4
-  | _ -> fprintf !oc "<hr/>\n"
-
-let start_verbatim () =
-  fprintf !oc "<pre>\n"
-
-let end_verbatim () =
-  fprintf !oc "</pre>\n"
-
-let start_comment () =
-  fprintf !oc "<span class=\"comment\">(*"
-
-let end_comment () =
-  fprintf !oc "*)</span>"
-
-let start_bracket () =
-  fprintf !oc "<span class=\"bracket\">"
-
-let end_bracket () =
-  fprintf !oc "</span>"
-
-let in_proof = ref false
-let proof_counter = ref 0
-
-let start_proof kwd =
-  in_proof := true;
-  incr proof_counter;
-  fprintf !oc
-  "<div class=\"toggleproof\" onclick=\"toggleDisplay('proof%d')\">%s</div>\n"
-    !proof_counter kwd;
-  fprintf !oc "<div class=\"proofscript\" id=\"proof%d\">\n" !proof_counter
-
-let end_proof kwd =
-  fprintf !oc "%s</div>\n" kwd;
-  in_proof := false
-
-let start_html_page modname =
-  fprintf !oc
-{|<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml">
-
-<head>
-<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
-<title>Module %s</title>
-<meta name="description" content="Documentation of Coq module %s" />
-<link href="coq2html.css" rel="stylesheet" type="text/css" />
-<script type="text/javascript" src="coq2html.js"> </script>
-</head>
-
-<body onload="hideAll('proofscript')">
-<h1 class="title">Module %s</h1>
-<div class="coq">
-|} modname modname modname
-
-let end_html_page () =
-  fprintf !oc
-{|</div>
-<div class="footer"><hr/>Generated by coq2html</div>
-</body>
-</html>
-|}
-
-}
-
-let space = [' ' '\t']
-let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']*
-let path = ident ("." ident)*
-let start_proof = ("Proof" space* ".") | ("Proof" space+ "with") | ("Next" space+ "Obligation.")
-let end_proof = "Qed." | "Defined." | "Save." | "Admitted." | "Abort."
-
-let xref = ['A'-'Z' 'a'-'z' '0'-'9' '_' '.']+ | "<>"
-let integer = ['0'-'9']+
-
-rule coq_bol = parse
-  | space* (start_proof as sp)
-      { start_proof sp;
-        skip_newline lexbuf }
-  | space* "(** " ("*"+ as sect)
-      { start_section sect;
-        doc lexbuf;
-        end_section sect;
-        skip_newline lexbuf }
-  | space* "(** "
-      { start_doc();
-        doc lexbuf;
-        end_doc();
-        skip_newline lexbuf }
-  | space* "(*"
-      { comment lexbuf;
-        skip_newline lexbuf }
-  | eof
-      { () }
-  | space* as s
-      { space s;
-        coq lexbuf }
-
-and skip_newline = parse
-  | space* "\n"
-      { coq_bol lexbuf }
-  | ""
-      { coq lexbuf }
-
-and coq = parse
-  | end_proof as ep
-      { end_proof ep;
-        skip_newline lexbuf }
-  | "(**r "
-      { start_doc_right();
-        doc lexbuf;
-        end_doc_right();
-        coq lexbuf }
-  | "(*"
-      { if !in_proof then start_comment();
-        comment lexbuf;
-        coq lexbuf }
-  | path as id
-      { ident (Lexing.lexeme_start lexbuf) id; coq lexbuf }
-  | "\n"
-      { newline(); coq_bol lexbuf }
-  | eof
-      { () }
-  | _ as c
-      { character c; coq lexbuf }
-
-and bracket = parse
-  | ']'
-      { () }
-  | '['
-      { character '['; bracket lexbuf; character ']'; bracket lexbuf }
-  | path as id
-      { ident (Lexing.lexeme_start lexbuf) id; bracket lexbuf }
-  | eof
-      { () }
-  | _ as c
-      { character c; bracket lexbuf }
-
-and comment = parse
-  | "*)"
-      { if !in_proof then end_comment() }
-  | "(*"
-      { if !in_proof then start_comment();
-        comment lexbuf; comment lexbuf }
-  | eof
-      { () }
-  | "\n"
-      { if !in_proof then newline();
-        comment lexbuf }
-  | space* as s
-      { if !in_proof then space s;
-        comment lexbuf }
-  | eof
-      { () }
-  | _ as c
-      { if !in_proof then character c;
-        comment lexbuf }
-
-and doc_bol = parse
-  | "<<" space* "\n"
-      { start_verbatim();
-        verbatim lexbuf;
-        end_verbatim();
-        doc_bol lexbuf }
-  | "-"+ as d
-      { dashes d; doc lexbuf }
-  | "\n"
-      { set_enum_depth 0; doc_bol lexbuf }
-  | ""
-      { doc lexbuf }
-
-and doc = parse
-  | "*)"
-      { () }
-  | "\n"
-      { character '\n'; doc_bol lexbuf }
-  | "["
-      { start_bracket(); bracket lexbuf; end_bracket(); doc lexbuf }
-  | "$" [^ '\n' '$']* "$"
-      { doc lexbuf }
-  | "#" ([^ '\n' '#']* as html) "#"
-      { output_string !oc html; doc lexbuf }
-  | eof
-      { () }
-  | _ as c
-      { character c; doc lexbuf }
-
-and verbatim = parse
-  | "\n>>" space* "\n"
-      { () }
-  | eof
-      { () }
-  | _ as c
-      { character c; verbatim lexbuf }
-
-and globfile = parse
-  | eof
-      { () }
-  | "F" (path as m) space* "\n"
-      { current_module := m; add_module m;
-        globfile lexbuf }
-  | "R" (integer as pos) ":" (integer)
-    space+ (xref as dp)
-    space+ (xref as sp)
-    space+ (xref as id)
-    space+ (ident as ty)
-    space* "\n"
-      { add_reference !current_module (int_of_string pos) dp sp id ty;
-        globfile lexbuf }
-  | (ident as ty)
-    space+ (integer as pos) ":" (integer)
-    space+ (xref as sp)
-    space+ (xref as id)
-    space* "\n"
-      { add_definition !current_module (int_of_string pos) sp id ty;
-        globfile lexbuf }
-  | [^ '\n']* "\n"
-      { globfile lexbuf }
-
-{
-
-let output_name = ref "-"
-
-let process_file f =
-  if Filename.check_suffix f ".v" then begin
-    let pref_f = Filename.chop_suffix f ".v" in
-    let base_f = Filename.basename pref_f in
-    current_module :=
-      "compcert." ^ Str.global_replace (Str.regexp "/") "." pref_f;
-    let ic = open_in f in
-    if !output_name = "-" then
-      oc := stdout
-    else
-      oc := open_out (Str.global_replace (Str.regexp "%") base_f !output_name);
-    start_html_page base_f;
-    coq_bol (Lexing.from_channel ic);
-    end_html_page();
-    if !output_name <> "-" then (close_out !oc; oc := stdout);
-    close_in ic
-  end else
-  if Filename.check_suffix f ".glob" then begin
-    current_module := "";
-    let ic = open_in f in
-    globfile (Lexing.from_channel ic);
-    close_in ic
-  end else begin
-    eprintf "Don't know what to do with file %s\n" f;
-    exit 2
-  end
-
-let _ =
-  Arg.parse [
-    "-o", Arg.String (fun s -> output_name := s),
-      " <output>   Set output file ('%' replaced by module name)"
-  ] process_file
-  "Usage: coq2html [options] <file.glob> file.v\nOptions are:"
-}
diff --git a/doc/coqdoc.css b/doc/coqdoc.css
deleted file mode 100644
index f2ae96da..00000000
--- a/doc/coqdoc.css
+++ /dev/null
@@ -1,62 +0,0 @@
-body {
-  color: black;
-  background: white;
-  margin-left: 15%;
-  margin-right: 5%;
-}
-
-#main  a.idref:visited {color : #416DFF; text-decoration : none; }
-#main  a.idref:link {color : #416DFF; text-decoration : none; }
-#main  a.idref:hover {text-decoration : none; }
-#main  a.idref:active {text-decoration : none; }
-
-#main  a.modref:visited {color : #416DFF; text-decoration : none; }
-#main  a.modref:link {color : #416DFF; text-decoration : none; }
-#main  a.modref:hover {text-decoration : none; }
-#main  a.modref:active {text-decoration : none; }
-
-#main .keyword { color : #cf1d1d }
-
-#main .doc {
-   margin-left: -5%;
-}
-
-#main span.docright {
-  position: absolute;
-  left: 60%;
-  width: 40%
-}
-
-h1.libtitle {
-  font-size: 2em;
-  margin-left: -15%;
-  margin-right: -5%;
-  text-align: center
-}
-
-h1 {
-  font-size: 1.5em;
-}
-h2 {
-  font-size: 1.17em;
-}
-
-h1, h2 {
-  font-family: sans-serif;
-}
-
-.doc code {
-  color: #008000;
-}
-
-/* Pied de page */
-
-hr { margin-left: -15%; margin-right:-5%; }
-
-#footer { font-size: 0.83em;
-          font-family: sans-serif; }
-
-#footer a:visited { color: blue; }
-#footer a:link { text-decoration: none; 
-                 color: #888888; }
-
diff --git a/doc/index.html b/doc/index.html
index 2ac5f698..60c4e9a0 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -69,73 +69,73 @@ following <A HREF="LICENSE">license</A>.
 <H3>General-purpose libraries, data structures and algorithms</H3>
 
 <UL>
-<LI> <A HREF="html/Coqlib.html">Coqlib</A>: addendum to the Coq standard library.
-<LI> <A HREF="html/Maps.html">Maps</A>: finite maps.
-<LI> <A HREF="html/Integers.html">Integers</A>: machine integers.
-<LI> <A HREF="html/Floats.html">Floats</A>: machine floating-point numbers.
-<LI> <A HREF="html/Iteration.html">Iteration</A>: various forms of "while" loops.
-<LI> <A HREF="html/Ordered.html">Ordered</A>: construction of
+<LI> <A HREF="html/compcert.lib.Coqlib.html">Coqlib</A>: addendum to the Coq standard library.
+<LI> <A HREF="html/compcert.lib.Maps.html">Maps</A>: finite maps.
+<LI> <A HREF="html/compcert.lib.Integers.html">Integers</A>: machine integers.
+<LI> <A HREF="html/compcert.lib.Floats.html">Floats</A>: machine floating-point numbers.
+<LI> <A HREF="html/compcert.lib.Iteration.html">Iteration</A>: various forms of "while" loops.
+<LI> <A HREF="html/compcert.lib.Ordered.html">Ordered</A>: construction of
 ordered types.
-<LI> <A HREF="html/Lattice.html">Lattice</A>: construction of
+<LI> <A HREF="html/compcert.lib.Lattice.html">Lattice</A>: construction of
 semi-lattices.
-<LI> <A HREF="html/Kildall.html">Kildall</A>: resolution of dataflow
+<LI> <A HREF="html/compcert.backend.Kildall.html">Kildall</A>: resolution of dataflow
 inequations by fixpoint iteration.
-<LI> <A HREF="html/UnionFind.html">UnionFind</A>: a persistent union-find data structure.
-<LI> <A HREF="html/Postorder.html">Postorder</A>: postorder numbering of a directed graph.
+<LI> <A HREF="html/compcert.lib.UnionFind.html">UnionFind</A>: a persistent union-find data structure.
+<LI> <A HREF="html/compcert.lib.Postorder.html">Postorder</A>: postorder numbering of a directed graph.
 </UL>
 
 <H3>Definitions and theorems used in many parts of the development</H3>
 
 <UL>
-<LI> <A HREF="html/Errors.html">Errors</A>: the Error monad.
-<LI> <A HREF="html/AST.html">AST</A>: identifiers, whole programs and other
+<LI> <A HREF="html/compcert.common.Errors.html">Errors</A>: the Error monad.
+<LI> <A HREF="html/compcert.common.AST.html">AST</A>: identifiers, whole programs and other
 common elements of abstract syntaxes.
-<LI> <A HREF="html/Linking.html">Linking</A>: generic framework to define syntactic linking over the CompCert languages.
-<LI> <A HREF="html/Values.html">Values</A>: run-time values.
-<LI> <A HREF="html/Events.html">Events</A>: observable events and traces.
-<LI> <A HREF="html/Memory.html">Memory</A>: memory model. <BR>
-See also: <A HREF="html/Memdata.html">Memdata</A> (in-memory representation of data).
-<LI> <A HREF="html/Globalenvs.html">Globalenvs</A>: global execution environments.
-<LI> <A HREF="html/Smallstep.html">Smallstep</A>: tools for small-step semantics.
-<LI> <A HREF="html/Behaviors.html">Behaviors</A>: from small-step semantics to observable behaviors of programs.
-<LI> <A HREF="html/Determinism.html">Determinism</A>: determinism properties of small-step semantics.
-<LI> <A HREF="html/Op.html"><I>Op</I></A>: operators, addressing modes and their
+<LI> <A HREF="html/compcert.common.Linking.html">Linking</A>: generic framework to define syntactic linking over the CompCert languages.
+<LI> <A HREF="html/compcert.common.Values.html">Values</A>: run-time values.
+<LI> <A HREF="html/compcert.common.Events.html">Events</A>: observable events and traces.
+<LI> <A HREF="html/compcert.common.Memory.html">Memory</A>: memory model. <BR>
+See also: <A HREF="html/compcert.common.Memdata.html">Memdata</A> (in-memory representation of data).
+<LI> <A HREF="html/compcert.common.Globalenvs.html">Globalenvs</A>: global execution environments.
+<LI> <A HREF="html/compcert.common.Smallstep.html">Smallstep</A>: tools for small-step semantics.
+<LI> <A HREF="html/compcert.common.Behaviors.html">Behaviors</A>: from small-step semantics to observable behaviors of programs.
+<LI> <A HREF="html/compcert.common.Determinism.html">Determinism</A>: determinism properties of small-step semantics.
+<LI> <A HREF="html/compcert.powerpc.Op.html"><I>Op</I></A>: operators, addressing modes and their
 semantics.
-<LI> <A HREF="html/Unityping.html">Unityping</A>: a solver for atomic unification constraints.
+<LI> <A HREF="html/compcert.common.Unityping.html">Unityping</A>: a solver for atomic unification constraints.
 </UL>
 
 <H3>Source, intermediate and target languages: syntax and semantics</H3>
 
 <UL>
 <LI> The CompCert C source language:
-<A HREF="html/Csyntax.html">syntax</A> and
-<A HREF="html/Csem.html">semantics</A> and
-<A HREF="html/Cstrategy.html">determinized semantics</A> and
-<A HREF="html/Ctyping.html">type system</A>.<BR>
-See also: <A HREF="html/Ctypes.html">type expressions</A> and
-<A HREF="html/Cop.html">operators (syntax and semantics)</A>.<BR>
-See also: <A HREF="html/Cexec.html">reference interpreter</A>.
-<LI> <A HREF="html/Clight.html">Clight</A>: a simpler version of CompCert C where expressions contain no side-effects.
-<LI> <A HREF="html/Csharpminor.html">Csharpminor</A>: low-level
+<A HREF="html/compcert.cfrontend.Csyntax.html">syntax</A> and
+<A HREF="html/compcert.cfrontend.Csem.html">semantics</A> and
+<A HREF="html/compcert.cfrontend.Cstrategy.html">determinized semantics</A> and
+<A HREF="html/compcert.cfrontend.Ctyping.html">type system</A>.<BR>
+See also: <A HREF="html/compcert.cfrontend.Ctypes.html">type expressions</A> and
+<A HREF="html/compcert.cfrontend.Cop.html">operators (syntax and semantics)</A>.<BR>
+See also: <A HREF="html/compcert.cfrontend.Cexec.html">reference interpreter</A>.
+<LI> <A HREF="html/compcert.cfrontend.Clight.html">Clight</A>: a simpler version of CompCert C where expressions contain no side-effects.
+<LI> <A HREF="html/compcert.cfrontend.Csharpminor.html">Csharpminor</A>: low-level
  structured language.
-<LI> <A HREF="html/Cminor.html">Cminor</A>: low-level structured
+<LI> <A HREF="html/compcert.backend.Cminor.html">Cminor</A>: low-level structured
 language, with explicit stack allocation of certain local variables.
-<LI> <A HREF="html/CminorSel.html">CminorSel</A>: like Cminor,
+<LI> <A HREF="html/compcert.backend.CminorSel.html">CminorSel</A>: like Cminor,
 with machine-specific operators and addressing modes.
-<LI> <A HREF="html/RTL.html">RTL</A>: register transfer language (3-address
+<LI> <A HREF="html/compcert.backend.RTL.html">RTL</A>: register transfer language (3-address
 code, control-flow graph, infinitely many pseudo-registers). <BR>
-See also: <A HREF="html/Registers.html">Registers</A> (representation of
+See also: <A HREF="html/compcert.backend.Registers.html">Registers</A> (representation of
 pseudo-registers).
-<LI> <A HREF="html/LTL.html">LTL</A>: location transfer language (3-address
+<LI> <A HREF="html/compcert.backend.LTL.html">LTL</A>: location transfer language (3-address
 code, control-flow graph of basic blocks, finitely many physical registers, infinitely
 many stack slots). <BR>
-See also: <A HREF="html/Locations.html">Locations</A> (representation of
-locations) and <A HREF="html/Machregs.html"><I>Machregs</I></A> (description of processor registers).
-<LI> <A HREF="html/Linear.html">Linear</A>: like LTL, but the CFG is
+See also: <A HREF="html/compcert.backend.Locations.html">Locations</A> (representation of
+locations) and <A HREF="html/compcert.powerpc.Machregs.html"><I>Machregs</I></A> (description of processor registers).
+<LI> <A HREF="html/compcert.backend.Linear.html">Linear</A>: like LTL, but the CFG is
 replaced by a linear list of instructions with explicit branches and labels.
-<LI> <A HREF="html/Mach.html">Mach</A>: like Linear, with a more concrete
+<LI> <A HREF="html/compcert.backend.Mach.html">Mach</A>: like Linear, with a more concrete
 view of the activation record.  
-<LI> <A HREF="html/Asm.html"><I>Asm</I></A>: abstract syntax for PowerPC assembly
+<LI> <A HREF="html/compcert.powerpc.Asm.html"><I>Asm</I></A>: abstract syntax for PowerPC assembly
 code.
 </UL>
 
@@ -153,170 +153,170 @@ code.
   <TD>Pulling side-effects out of expressions;<br>
       fixing an evaluation order</TD>
   <TD>CompCert C to Clight</TD>
-  <TD><A HREF="html/SimplExpr.html">SimplExpr</A></TD>
-  <TD><A HREF="html/SimplExprspec.html">SimplExprspec</A><br>
-      <A HREF="html/SimplExprproof.html">SimplExprproof</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.SimplExpr.html">SimplExpr</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.SimplExprspec.html">SimplExprspec</A><br>
+      <A HREF="html/compcert.cfrontend.SimplExprproof.html">SimplExprproof</A></TD>
 </TR>
 <TR valign="top">
   <TD>Pulling non-adressable scalar local variables out of memory</TD>
   <TD>Clight to Clight</TD>
-  <TD><A HREF="html/SimplLocals.html">SimplLocals</A></TD>
-  <TD><A HREF="html/SimplLocalsproof.html">SimplLocalsproof</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.SimplLocals.html">SimplLocals</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.SimplLocalsproof.html">SimplLocalsproof</A></TD>
 </TR>
 <TR valign="top">
   <TD>Simplification of control structures; <br>
       explication of type-dependent computations</TD>
   <TD>Clight to Csharpminor</TD>
-  <TD><A HREF="html/Cshmgen.html">Cshmgen</A></TD>
-  <TD><A HREF="html/Cshmgenproof.html">Cshmgenproof</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.Cshmgen.html">Cshmgen</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.Cshmgenproof.html">Cshmgenproof</A></TD>
 </TR>
 <TR valign="top">
   <TD>Stack allocation of local variables<br>
       whose address is taken;<br>
       simplification of switch statements</TD>
   <TD>Csharpminor to Cminor</TD>
-  <TD><A HREF="html/Cminorgen.html">Cminorgen</A></TD>
-  <TD><A HREF="html/Cminorgenproof.html">Cminorgenproof</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.Cminorgen.html">Cminorgen</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.Cminorgenproof.html">Cminorgenproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Recognition of operators<br>and addressing modes</TD>
   <TD>Cminor to CminorSel</TD>
-  <TD><A HREF="html/Selection.html">Selection</A><br>
-      <A HREF="html/SelectOp.html"><I>SelectOp</I></A><br>
-      <A HREF="html/SelectLong.html"><I>SelectLong</I></A><br>
-      <A HREF="html/SelectDiv.html">SelectDiv</A><br>
-      <A HREF="html/SplitLong.html">SplitLong</A></TD>
-  <TD><A HREF="html/Selectionproof.html">Selectionproof</A><br>
-      <A HREF="html/SelectOpproof.html"><I>SelectOpproof</I></A><br>
-      <A HREF="html/SelectLongproof.html"><I>SelectLongproof</I></A><br>
-      <A HREF="html/SelectDivproof.html">SelectDivproof</A><br>
-      <A HREF="html/SplitLongproof.html">SplitLongproof</A></TD>
+  <TD><A HREF="html/compcert.backend.Selection.html">Selection</A><br>
+      <A HREF="html/Selectcompcert.powerpc.Op.html"><I>SelectOp</I></A><br>
+      <A HREF="html/compcert.powerpc.SelectLong.html"><I>SelectLong</I></A><br>
+      <A HREF="html/compcert.backend.SelectDiv.html">SelectDiv</A><br>
+      <A HREF="html/compcert.backend.SplitLong.html">SplitLong</A></TD>
+  <TD><A HREF="html/compcert.backend.Selectionproof.html">Selectionproof</A><br>
+      <A HREF="html/compcert.powerpc.SelectOpproof.html"><I>SelectOpproof</I></A><br>
+      <A HREF="html/compcert.powerpc.SelectLongproof.html"><I>SelectLongproof</I></A><br>
+      <A HREF="html/compcert.backend.SelectDivproof.html">SelectDivproof</A><br>
+      <A HREF="html/compcert.backend.SplitLongproof.html">SplitLongproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Construction of the CFG, <br>3-address code generation</TD>
   <TD>CminorSel to RTL</TD>
-  <TD><A HREF="html/RTLgen.html">RTLgen</A></TD>
-  <TD><A HREF="html/RTLgenspec.html">RTLgenspec</A><BR>
-      <A HREF="html/RTLgenproof.html">RTLgenproof</A></TD>
+  <TD><A HREF="html/compcert.backend.RTLgen.html">RTLgen</A></TD>
+  <TD><A HREF="html/compcert.backend.RTLgenspec.html">RTLgenspec</A><BR>
+      <A HREF="html/compcert.backend.RTLgenproof.html">RTLgenproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Recognition of tail calls</TD>
   <TD>RTL to RTL</TD>
-  <TD><A HREF="html/Tailcall.html">Tailcall</A></TD>
-  <TD><A HREF="html/Tailcallproof.html">Tailcallproof</A></TD>
+  <TD><A HREF="html/compcert.backend.Tailcall.html">Tailcall</A></TD>
+  <TD><A HREF="html/compcert.backend.Tailcallproof.html">Tailcallproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Function inlining</TD>
   <TD>RTL to RTL</TD>
-  <TD><A HREF="html/Inlining.html">Inlining</A></TD>
-  <TD><A HREF="html/Inliningspec.html">Inliningspec</A><BR>
-      <A HREF="html/Inliningproof.html">Inliningproof</A></TD>
+  <TD><A HREF="html/compcert.backend.Inlining.html">Inlining</A></TD>
+  <TD><A HREF="html/compcert.backend.Inliningspec.html">Inliningspec</A><BR>
+      <A HREF="html/compcert.backend.Inliningproof.html">Inliningproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Postorder renumbering of the CFG</TD>
   <TD>RTL to RTL</TD>
-  <TD><A HREF="html/Renumber.html">Renumber</A></TD>
-  <TD><A HREF="html/Renumberproof.html">Renumberproof</A></TD>
+  <TD><A HREF="html/compcert.backend.Renumber.html">Renumber</A></TD>
+  <TD><A HREF="html/compcert.backend.Renumberproof.html">Renumberproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Constant propagation</TD>
   <TD>RTL to RTL</TD>
-  <TD><A HREF="html/Constprop.html">Constprop</A><br>
-      <A HREF="html/ConstpropOp.html"><I>ConstpropOp</I></A></TD>
-  <TD><A HREF="html/Constpropproof.html">Constpropproof</A><br>
-      <A HREF="html/ConstpropOpproof.html"><I>ConstproppOproof</I></A></TD>
+  <TD><A HREF="html/compcert.backend.Constprop.html">Constprop</A><br>
+      <A HREF="html/compcert.powerpc.Constpropcompcert.powerpc.Op.html"><I>ConstpropOp</I></A></TD>
+  <TD><A HREF="html/compcert.backend.Constpropproof.html">Constpropproof</A><br>
+      <A HREF="html/compcert.powerpc.ConstpropOpproof.html"><I>ConstproppOproof</I></A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Common subexpression elimination</TD>
   <TD>RTL to RTL</TD>
-  <TD><A HREF="html/CSE.html">CSE</A><BR>
-      <A HREF="html/CombineOp.html"><I>CombineOp</I></A></TD>
-  <TD><A HREF="html/CSEproof.html">CSEproof</A><BR>
-      <A HREF="html/CombineOpproof.html"><I>CombineOpproof</I></A></TD>
+  <TD><A HREF="html/compcert.backend.CSE.html">CSE</A><BR>
+      <A HREF="html/compcert.powerpc.Combinecompcert.powerpc.Op.html"><I>CombineOp</I></A></TD>
+  <TD><A HREF="html/compcert.backend.CSEproof.html">CSEproof</A><BR>
+      <A HREF="html/compcert.powerpc.CombineOpproof.html"><I>CombineOpproof</I></A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Redundancy elimination</TD>
   <TD>RTL to RTL</TD>
-  <TD><A HREF="html/Deadcode.html">Deadcode</A></TD>
-  <TD><A HREF="html/Deadcodeproof.html">Deadcodeproof</A></TD>
+  <TD><A HREF="html/compcert.backend.Deadcode.html">Deadcode</A></TD>
+  <TD><A HREF="html/compcert.backend.Deadcodeproof.html">Deadcodeproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Removal of unused static globals</TD>
   <TD>RTL to RTL</TD>
-  <TD><A HREF="html/Unusedglob.html">Unusedglob</A></TD>
-  <TD><A HREF="html/Unusedglobproof.html">Unusedglobproof</A></TD>
+  <TD><A HREF="html/compcert.backend.Unusedglob.html">Unusedglob</A></TD>
+  <TD><A HREF="html/compcert.backend.Unusedglobproof.html">Unusedglobproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Register allocation (validation a posteriori)</TD>
   <TD>RTL to LTL</TD>
-  <TD><A HREF="html/Allocation.html">Allocation</A></TD>
-  <TD><A HREF="html/Allocproof.html">Allocproof</A></TD>
+  <TD><A HREF="html/compcert.backend.Allocation.html">Allocation</A></TD>
+  <TD><A HREF="html/compcert.backend.Allocproof.html">Allocproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Branch tunneling</TD>
   <TD>LTL to LTL</TD>
-  <TD><A HREF="html/Tunneling.html">Tunneling</A></TD>
-  <TD><A HREF="html/Tunnelingproof.html">Tunnelingproof</A></TD>
+  <TD><A HREF="html/compcert.backend.Tunneling.html">Tunneling</A></TD>
+  <TD><A HREF="html/compcert.backend.Tunnelingproof.html">Tunnelingproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Linearization of the CFG</TD>
   <TD>LTL to Linear</TD>
-  <TD><A HREF="html/Linearize.html">Linearize</A></TD>
-  <TD><A HREF="html/Linearizeproof.html">Linearizeproof</A></TD>
+  <TD><A HREF="html/compcert.backend.Linearize.html">Linearize</A></TD>
+  <TD><A HREF="html/compcert.backend.Linearizeproof.html">Linearizeproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Removal of unreferenced labels</TD>
   <TD>Linear to Linear</TD>
-  <TD><A HREF="html/CleanupLabels.html">CleanupLabels</A></TD>
-  <TD><A HREF="html/CleanupLabelsproof.html">CleanupLabelsproof</A></TD>
+  <TD><A HREF="html/compcert.backend.CleanupLabels.html">CleanupLabels</A></TD>
+  <TD><A HREF="html/compcert.backend.CleanupLabelsproof.html">CleanupLabelsproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Synthesis of debugging information</TD>
   <TD>Linear to Linear</TD>
-  <TD><A HREF="html/Debugvar.html">Debugvar</A></TD>
-  <TD><A HREF="html/Debugvarproof.html">Debugvarproof</A></TD>
+  <TD><A HREF="html/compcert.backend.Debugvar.html">Debugvar</A></TD>
+  <TD><A HREF="html/compcert.backend.Debugvarproof.html">Debugvarproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Laying out the activation records</TD>
   <TD>Linear to Mach</TD>
-  <TD><A HREF="html/Stacking.html">Stacking</A><BR>
-      <A HREF="html/Bounds.html">Bounds</A><BR>
-      <A HREF="html/Stacklayout.html"><I>Stacklayout</I></A></TD>
-  <TD><A HREF="html/Stackingproof.html">Stackingproof</A><br>
-      <A HREF="html/Separation.html">Separation</A></TD>
+  <TD><A HREF="html/compcert.backend.Stacking.html">Stacking</A><BR>
+      <A HREF="html/compcert.backend.Bounds.html">Bounds</A><BR>
+      <A HREF="html/compcert.powerpc.Stacklayout.html"><I>Stacklayout</I></A></TD>
+  <TD><A HREF="html/compcert.backend.Stackingproof.html">Stackingproof</A><br>
+      <A HREF="html/compcert.common.Separation.html">Separation</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Emission of assembly code</TD>
   <TD>Mach to Asm</TD>
-  <TD><A HREF="html/Asmgen.html"><I>Asmgen</I></A></TD>
-  <TD><A HREF="html/Asmgenproof0.html"><I>Asmgenproof0</I></A><BR>
-      <A HREF="html/Asmgenproof1.html"><I>Asmgenproof1</I></A><BR>
-      <A HREF="html/Asmgenproof.html"><I>Asmgenproof</I></A></TD>
+  <TD><A HREF="html/compcert.powerpc.Asmgen.html"><I>Asmgen</I></A></TD>
+  <TD><A HREF="html/compcert.backend.Asmgenproof0.html"><I>Asmgenproof0</I></A><BR>
+      <A HREF="html/compcert.powerpc.Asmgenproof1.html"><I>Asmgenproof1</I></A><BR>
+      <A HREF="html/compcert.powerpc.Asmgenproof.html"><I>Asmgenproof</I></A></TD>
 </TR>
 </TABLE>
 
 <H3>All together</H3>
 
 <UL>
-<LI> <A HREF="html/Compiler.html">Compiler</A>: composing the passes together;
+<LI> <A HREF="html/compcert.driver.Compiler.html">Compiler</A>: composing the passes together;
 whole-compiler semantic preservation theorems.
-<LI> <A HREF="html/Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems.
+<LI> <A HREF="html/compcert.driver.Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems.
 </UL>
 
 <H3>Static analyses</H3>
@@ -325,23 +325,23 @@ The following static analyses are performed over the RTL intermediate
 representation to support optimizations such as constant propagation,
 CSE, and dead code elimination.
 <UL>
-<LI> <A HREF="html/Liveness.html">Liveness</A>: liveness analysis</A>.
-<LI> <A HREF="html/ValueAnalysis.html">ValueAnalysis</A>: value and alias analysis</A> <BR>
-See also: <A HREF="html/ValueDomain.html">ValueDomain</A>: the abstract domain for value analysis.<BR>
-See also: <A HREF="html/ValueAOp.html"><I>ValueAOp</I></A>: processor-dependent parts of value analysis.
-<LI> <A HREF="html/Deadcode.html">Deadcode</A>: neededness analysis</A> <BR>
-See also: <A HREF="html/NeedDomain.html">NeedDomain</A>: the abstract domain for neededness analysis.<BR>
-See also: <A HREF="html/NeedOp.html"><I>NeedOp</I></A>: processor-dependent parts of neededness analysis.
+<LI> <A HREF="html/compcert.backend.Liveness.html">Liveness</A>: liveness analysis</A>.
+<LI> <A HREF="html/compcert.backend.ValueAnalysis.html">ValueAnalysis</A>: value and alias analysis</A> <BR>
+See also: <A HREF="html/compcert.backend.ValueDomain.html">ValueDomain</A>: the abstract domain for value analysis.<BR>
+See also: <A HREF="html/ValueAcompcert.powerpc.Op.html"><I>ValueAOp</I></A>: processor-dependent parts of value analysis.
+<LI> <A HREF="html/compcert.backend.Deadcode.html">Deadcode</A>: neededness analysis</A> <BR>
+See also: <A HREF="html/compcert.backend.NeedDomain.html">NeedDomain</A>: the abstract domain for neededness analysis.<BR>
+See also: <A HREF="html/compcert.powerpc.Needcompcert.powerpc.Op.html"><I>NeedOp</I></A>: processor-dependent parts of neededness analysis.
 </UL>
 
 <H3>Type systems</H3>
 
-The <A HREF="html/Ctyping.html">type system of CompCert C</A> is fully formalized.  For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions.
+The <A HREF="html/compcert.cfrontend.Ctyping.html">type system of CompCert C</A> is fully formalized.  For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions.
 <UL>
-<LI> <A HREF="html/Ctyping.html">RTLtyping</A>: typing for CompCert C + type-checking functions.
-<LI> <A HREF="html/RTLtyping.html">RTLtyping</A>: typing for RTL + type
+<LI> <A HREF="html/compcert.cfrontend.Ctyping.html">RTLtyping</A>: typing for CompCert C + type-checking functions.
+<LI> <A HREF="html/compcert.backend.RTLtyping.html">RTLtyping</A>: typing for RTL + type
 reconstruction.
-<LI> <A HREF="html/Lineartyping.html">Lineartyping</A>: typing for Linear.
+<LI> <A HREF="html/compcert.backend.Lineartyping.html">Lineartyping</A>: typing for Linear.
 </UL>
 
 <HR>