Add more documentation and add coqdoc stylesheet

6 files changed, 928 insertions, 3 deletions

diff --git a/Makefile b/Makefile
index 5577ba9..9c40941 100644
--- a/Makefile
+++ b/Makefile
@@ -50,6 +50,10 @@ proof: Makefile.coq
 
 doc: Makefile.coq
 	$(MAKE) COQDOCFLAGS="$(COQDOCFLAGS)" -f Makefile.coq html
+	cp ./docs/res/coqdoc.css html/.
+
+doc-pdf: Makefile.coq
+	$(MAKE) COQDOCFLAGS="$(COQDOCFLAGS)" -f Makefile.coq all.tex
 
 extraction: src/extraction/STAMP
 
diff --git a/docs/common.org b/docs/common.org
index 8c39be0..aa27264 100644
--- a/docs/common.org
+++ b/docs/common.org
@@ -4,6 +4,8 @@
 #+macro: version 1.2.2
 #+macro: modified 2022-02-24
 
+#+macro: base_url https://vericert.ymhg.org
+
 #+macro: link src_emacs-lisp[:results raw]{(ymhg/link "$1" "$2")}
 
 #+macro: texinfo_head (eval (if (eq org-export-current-backend 'texinfo) "#+exclude_tags: noexport_texinfo" "#+exclude_tags: onlyexport_texinfo"))
diff --git a/docs/documentation.org b/docs/documentation.org
index d4ef799..3a0633f 100644
--- a/docs/documentation.org
+++ b/docs/documentation.org
@@ -18,7 +18,7 @@ application-specific integrated circuit (ASIC).
 #+attr_html: :width 600
 #+caption: Current design of Vericert, where HTL is an intermediate language representing a finite state machine with data-path (FSMD) and Verilog is the target language.
 #+name: fig:design
-[[/images/toolflow.svg]]
+[[./images/toolflow.svg]]
 
 The design shown in Figure [[fig:design]] shows how Vericert leverages an existing verified C compiler
 called [[https://compcert.org/compcert-C.html][CompCert]] to perform this translation.
@@ -554,4 +554,4 @@ A small standalone Coq file that exhibits many of the style points.
 :appendix: t
 :END:
 
-#+include: fdl.org
+#+include: res/fdl.org
diff --git a/docs/man.org b/docs/man.org
index 279165c..36dbc42 100644
--- a/docs/man.org
+++ b/docs/man.org
@@ -12,7 +12,59 @@ vericert - A formally verified high-level synthesis tool.
 
 * DESCRIPTION
 
-- -drtl :: Print intermediate RTL.
+** HLS Options
+
+- --no-hls :: Do not use HLS and generate standard flow
+- --simulate :: Simulate the result with the Verilog semantics
+- --debug-hls :: Add debug logic to the Verilog
+- --initialise-stack :: initialise the stack to all 0s
+
+** HLS Optimisations
+
+- -fschedule :: Schedule the resulting hardware [off]
+- -fif-conversion :: If-conversion optimisation [off]
+
+** General options
+
+- -stdlib <dir> :: Set the path of the Compcert run-time library
+- -v :: Print external commands before invoking them
+- -timings :: Show the time spent in various compiler passes
+- -version :: Print the version string and exit
+- -target <value> :: Generate code for the given target
+- -conf <file> :: Read configuration from file
+- @<file> :: Read command line options from <file>
+
+** Tracing Options
+
+- -dprepro :: Save C file after preprocessing in <file>.i
+- -dparse :: Save C file after parsing and elaboration in <file>.parsed.c
+- -dc :: Save generated C in <file>.compcert.c
+- -dclight :: Save generated Clight in <file>.light.c
+- -dcminor :: Save generated Cminor in <file>.cm
+- -drtl :: Save RTL at various optimization points in <file>.rtl.<n>
+- -drtlblock :: Save RTLBlock <file>.rtlblock
+- -dhtl :: Save HTL before Verilog generation <file>.htl
+- -dltl :: Save LTL after register allocation in <file>.ltl
+- -dmach :: Save generated Mach code in <file>.mach
+- -dasm :: Save generated assembly in <file>.s
+- -dall :: Save all generated intermediate files in <file>.<ext>
+- -sdump :: Save info for post-linking validation in <file>.json
+- -o <file> :: Generate output in <file>
+
+** Diagnostic options
+
+- -Wall :: Enable all warnings
+- -W<warning> :: Enable the specific <warning>
+- -Wno-<warning> :: Disable the specific <warning>
+- -Werror :: Make all warnings into errors
+- -Werror=<warning> :: Turn <warning> into an error
+- -Wno-error=<warning> :: Turn <warning> into a warning even if -Werror is specified
+- -Wfatal-errors :: Turn all errors into fatal errors aborting the compilation
+- -fdiagnostics-color :: Turn on colored diagnostics
+- -fno-diagnostics-color :: Turn of colored diagnostics
+- -fmax-errors=<n> :: Maximum number of errors to report
+- -fdiagnostics-show-option :: Print the option name with mappable diagnostics
+- -fno-diagnostics-show-option :: Turn of printing of options with mappable diagnostics
 
 * AUTHOR
 
diff --git a/docs/res/coqdoc.css b/docs/res/coqdoc.css
new file mode 100644
index 0000000..5572aaa
--- /dev/null
+++ b/docs/res/coqdoc.css
@@ -0,0 +1,867 @@
+body {
+    padding: 0px 0px;
+    margin: 0px 0px;
+    padding-left: 1em;
+    background-color: white;
+    font-family: sans-serif;
+    background-repeat: no-repeat;
+    background-size: 100%;
+}
+
+#page {
+    display: block;
+    padding: 0px;
+    margin: 0px;
+}
+
+#header {
+    min-height: 100px;
+    max-width: 760px;
+    margin: 0 auto;
+    padding-left: 80px;
+    padding-right: 80px;
+    padding-top: 30px;
+}
+
+#header h1 {
+    padding: 0;
+    margin: 0;
+}
+
+/* Menu */
+ul#menu {
+    padding: 0;
+    display: block;
+    margin: auto;
+}
+
+ul#menu li, div.button {
+    display: inline-block;
+    background-color: white;
+    padding: 5px;
+    font-size: .70em;
+    text-transform: uppercase;
+    width: 30%;
+    text-align: center;
+    font-weight: 600;
+}
+
+div.button {
+        margin-top:5px;
+    width: 40%;
+}
+
+#button_block {margin-top:50px;}
+
+ul#menu a.hover li  {
+    background-color: red;
+}
+
+/* Contents */
+
+#main, #main_home {
+    display: block;
+    padding: 80px;
+    padding-top: 60px; /* BCP */
+    font-size: 100%;
+    line-height: 100%;
+    max-width: 760px;
+    background-color: #ffffff;
+    margin: 0 auto;
+}
+
+#main_home {
+    background-color: rgba(255, 255, 255, 0.5);
+}
+
+#index_content div.intro p {
+    font-size: 12px;
+}
+
+#main  h1 {
+    /* line-height: 80%; */
+    line-height: normal;
+    padding-top: 3px;
+    padding-bottom: 4px;
+    /* Demitri: font-size: 22pt; */
+    font-size: 200%; /* BCP */
+}
+
+/* allow for multi-line headers */
+#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 : #697f2f }
+#main { color: black }
+
+/* General section class - applies to all .section IDs */
+.section {
+    padding-top: 12px;
+    padding-bottom: 11px;
+    padding-left: 8px;
+    margin-top: 5px;
+    margin-bottom: 3px;
+    margin-top: 18px;
+    font-size : 125%;
+    color: #ffffff;
+}
+
+/* Book title in header */
+.booktitleinheader {
+    color: #000000;
+    text-transform: uppercase;
+    font-weight: 300;
+    letter-spacing: 1px;
+    font-size: 125%;
+    margin-left: 0px;
+    margin-bottom: 22px;
+ }
+
+/* Chapter titles */
+.libtitle {
+    max-width: 860px;
+    text-transform: uppercase;
+    margin: 5px auto;
+    font-weight: 500;
+    padding-bottom: 2px;
+    font-size: 120%;
+    letter-spacing: 3px;
+ }
+
+.subtitle {
+    display: block;
+    padding-top: 10px;
+    font-size: 70%;
+    line-height: normal;
+}
+
+h2.section {
+    color: #2a2c71;
+    background-color: transparent;
+    padding-left: 0px;
+    padding-top: 0px;
+    padding-bottom: 0px;
+    /* margin-top: 0px; */
+    margin-top: 9px; /* BCP 2/20 */
+    font-size : 135%; }
+
+h3.section {
+    /* background-color: rgb(90%,90%,100%); */
+    background-color: white;
+    /* padding-left: 8px; */
+    padding-left: 0px;
+    /* padding-top: 7px;  */
+    padding-top: 0px;
+    /* padding-bottom: 0px; */
+    padding-bottom: 0.5em;
+    /* margin-top: 9px; */
+    /* margin-top: 4px;  (BCP 2/20) */
+    margin-top: 9px;   /* BCP 2/20 */
+    font-size : 115%;
+    color:black;
+}
+
+h4.section {
+    margin-top: .2em;
+    background-color: white;
+    color: #2a2c71;
+    padding-left: 0px;
+    padding-top: 0px;
+    padding-bottom: 0.5em; /* 0px;  */
+    font-size : 100%;
+    font-style : bold;
+    text-decoration : underline;
+}
+
+#header p {
+    font-size: 13px;
+}
+
+/* Sets up Main ID and margins */
+
+#main .doc {
+    margin: 0px auto;
+    font-size: 14px;
+    line-height: 22px;
+    /* max-width: 570px; */
+    color: black;
+    /* text-align: justify; */
+    border-style: plain;
+    /* This might work better after changing back to standard coqdoc: */
+    padding-top: 10px;
+    /* padding-top: 18px; */
+}
+
+.quote {
+    margin-left: auto;
+    margin-right: auto;
+    width: 40em;
+    color: darkred;
+}
+
+.loud {
+    color: darkred;
+}
+
+pre {
+    margin-top: 0px;
+    margin-bottom: 0px;
+}
+
+.inlinecode {
+    display: inline;
+    /* font-size: 125%; */
+    color: #444444;
+    font-family: monospace }
+
+.doc .inlinecode {
+    display: inline;
+    font-size: 105%;
+    color: rgb(35%,35%,70%);
+    font-family: monospace }
+
+.doc .inlinecode .id {
+/* I am changing this to white in style below:
+    color: rgb(35%,35%,70%);
+*/
+}
+
+h1 .inlinecode .id, h1.section span.inlinecode {
+        color: #ffffff;
+}
+
+.inlinecodenm {
+    display: inline;
+    /* font-size: 125%; */
+    color: #444444;
+}
+
+.doc .inlinecodenm {
+    display: inline;
+    color: rgb(35%,35%,70%);
+}
+
+.doc .inlinecodenm .id {
+    color: rgb(35%,35%,70%);
+}
+
+.doc .code {
+    display: inline;
+    font-size: 110%;
+    color: rgb(35%,35%,70%);
+    font-family: monospace;
+    padding-left: 0px;
+}
+
+.comment {
+    display: inline;
+    font-family: monospace;
+    color: rgb(50%,50%,80%);
+}
+
+.inlineref {
+    display: inline;
+    /* font-family: monospace; */
+    color: rgb(50%,50%,80%);
+}
+
+.show::before {
+    /* content: "more"; */
+    content: "+";
+}
+
+.show {
+    background-color: rgb(93%,93%,93%);
+    display: inline;
+    font-family: monospace;
+    font-size: 60%;
+    padding-top: 1px;
+    padding-bottom: 2px;
+    padding-left: 4px;
+    padding-right: 4px;
+    color: rgb(60%,60%,60%);
+}
+
+/*
+.show {
+    display: inline;
+    font-family: monospace;
+    font-size: 60%;
+    padding-top: 0px;
+    padding-bottom: 0px;
+    padding-left: 10px;
+    border: 1px;
+    border-style: solid;
+    color: rgb(75%,75%,85%);
+}
+*/
+
+.proofbox {
+    font-size: 90%;
+    color: rgb(75%,75%,75%);
+}
+
+#main .less-space {
+    margin-top: -12px;
+}
+
+/* Inline quizzes */
+.quiz:before {
+    color: rgb(40%,40%,40%);
+    /* content: "- Quick Check -" ; */
+    display: block;
+    text-align: center;
+    margin-bottom: 5px;
+}
+.quiz {
+    border: 4px;
+    border-color: rgb(80%,80%,80%);
+    /*
+    margin-left: 40px;
+    margin-right: 100px;
+   */
+    padding: 5px;
+    padding-left: 8px;
+    padding-right: 8px;
+    margin-top: 10px;
+    margin-bottom: 15px;
+    border-style: solid;
+}
+
+/* For textual ones... */
+.show-old {
+    display: inline;
+    font-family: monospace;
+    font-size: 80%;
+    padding-top: 0px;
+    padding-bottom: 0px;
+    padding-left: 3px;
+    padding-right: 3px;
+    border: 1px;
+    margin-top: 5px;   /* doesn't work?! */
+    border-style: solid;
+    color: rgb(75%,75%,85%);
+}
+
+.largebr {
+    margin-top: 10px;
+}
+
+.code {
+    padding-left: 20px;
+    font-size: 14px;
+    font-family: monospace;
+    line-height: 17px;
+    margin-top: 9px;
+}
+
+/* Working:
+.code {
+    display: block;
+    padding-left: 0px;
+    font-size: 110%;
+    font-family: monospace;
+ }
+*/
+
+.code-space {
+    max-width: 50em;
+    margin-top: 0em;
+    /* margin-bottom: -.5em; */
+    margin-left: auto;
+    margin-right: auto;
+}
+
+.code-tight {
+    max-width: 50em;
+    margin-top: .6em;
+    /* margin-bottom: -.7em; */
+    margin-left: auto;
+    margin-right: auto;
+}
+
+hr.doublespaceincode {
+    height: 1pt;
+    visibility: hidden;
+    font-size: 10px;
+}
+
+/*
+code.br {
+  height: 5em;
+}
+*/
+
+#main .citation {
+    color: rgb(70%,0%,0%);
+    text-decoration: underline;
+}
+
+table.infrule {
+    border: 0px;
+    margin-left: 50px;
+    margin-top: .5em;
+    margin-bottom: 1.2em;
+}
+
+td.infrule {
+    font-family: monospace;
+    text-align: center;
+    /*    color: rgb(35%,35%,70%);  */
+    padding: 0px;
+    line-height: 100%;
+}
+
+tr.infrulemiddle hr {
+    margin: 1px 0 1px 0;
+}
+
+.infrulenamecol {
+    color: rgb(60%,60%,60%);
+    font-size: 80%;
+    padding-left: 1em;
+    padding-bottom: 0.1em
+}
+
+#footer {
+    font-size: 65%;
+    font-family: sans-serif;
+}
+
+.id { display: inline; }
+
+.id[title="constructor"] {
+    color: #697f2f;
+}
+
+.id[title="var"],
+.id[title="variable"] {
+    color: rgb(40%,0%,40%);
+}
+
+.id[title="definition"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="abbreviation"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="lemma"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="instance"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="projection"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="method"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="inductive"] {
+    color: #034764;
+}
+
+.id[title="record"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[title="class"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[title="keyword"] {
+    color : #697f2f;
+    /*     color: black; */
+}
+
+.inlinecode .id {
+    color: rgb(0%,0%,0%);
+}
+
+.nowrap {
+    white-space: nowrap;
+}
+
+.HIDEFROMHTML {
+    display: none;
+}
+
+/* TOC */
+
+#toc h2 {
+/*    padding-top: 13px; */
+    padding-bottom: 13px;
+    padding-left: 8px;
+    margin-top: 5px;
+    margin-top: 20px;
+    /* OLD: padding: 10px;
+       line-height: 120%;
+       background-color: rgb(60%,60%,100%); */
+}
+
+#toc h2.ui-accordion-header {
+    padding: .5em .5em .5em .7em;
+    outline: none;
+}
+
+#toc .ui-accordion .ui-accordion-content {
+        padding: 0.5em 2.5em 0.8em .9em;
+        border-top: 0;
+    margin-bottom: 1em;
+    /* bottom rule */
+    border: none;
+    border-bottom: 1px solid transparent;
+    transition: border-bottom-color 0.25s ease-in;
+    transition-delay: 0.15s;
+}
+
+#toc .ui-accordion .ui-accordion-content-active {
+    border-bottom: 1px solid #9b9b9b;
+    transition-delay: 0s;
+}
+
+#toc h2.ui-accordion-header-active {
+    background: silver !important;
+}
+
+#toc h2:not(.ui-accordion-header-active):hover {
+    background: rgba(0,0,0,0.04) !important;
+}
+
+#toc h2 a:hover {
+    text-decoration: underline;
+}
+
+#toc h2:hover::after {
+    content: "expand ▾";
+    font-size: 80%;
+    float: right;
+    margin-top: 0.2em;
+    color: silver;
+    opacity: 1;
+    transition: opacity .5s ease-in-out;
+}
+
+#toc h2.ui-accordion-header-active:hover::after {
+    opacity: 0;
+}
+
+#toc h2 .select { background-image: url('media/image/arrow_down.jpg'); }
+div#sec1.hide { display: none; }
+
+#toc ul {
+    padding-top: 8px;
+    font-size: 14px;
+    padding-left: 0;
+}
+
+#toc ul ul {
+    margin-bottom: -8px;
+}
+
+#toc li {
+    font-weight: 600;
+    list-style-type: none;
+    padding-top: 12px;
+    padding-bottom: 8px;
+}
+
+#toc li li {
+    font-weight: 300;
+    list-style-type: circle;
+    padding-bottom: 3px;
+    padding-top: 0px;
+    margin-left: 19px;
+}
+
+
+
+
+/*  Accordion Overrides  */
+
+/*  Widget Bar  */
+.ui-state-default,
+.ui-widget-content .ui-state-default,
+.ui-widget-header .ui-state-default,
+.ui-button,
+/* We use html here because we need a greater specificity to make sure disabled
+   works properly when clicked or hovered */
+html .ui-button.ui-state-disabled:hover,
+html .ui-button.ui-state-disabled:active {
+    border: none!important;
+    /* BCP 3/17: I like it better without the rules...
+       border-bottom: 1px solid silver!important; */
+    background: white !important;
+    font-weight: normal;
+    color: #454545!important;
+    font-weight: 400!important;
+    margin-top: 0px!important;
+
+}
+
+/* Misc visuals
+----------------------------------*/
+
+/* Corner radius */
+.ui-corner-all,
+.ui-corner-top,
+.ui-corner-left,
+.ui-corner-tl {
+ border-top-left-radius: 0px!important;
+}
+
+.ui-corner-all,
+.ui-corner-top,
+.ui-corner-right,
+.ui-corner-tr {
+ border-top-right-radius: 0px!important;
+}
+
+.ui-corner-all,
+.ui-corner-bottom,
+.ui-corner-left,
+.ui-corner-bl {
+ border-bottom-left-radius: 0px!important;
+}
+
+.ui-corner-all,
+.ui-corner-bottom,
+.ui-corner-right,
+.ui-corner-br {
+    border-bottom-right-radius: 0px!important;
+}
+
+html .ui-button.ui-state-disabled:focus {
+        color: red!important;
+}
+
+/*  Remove Icon  */
+.ui-icon { display: none!important; }
+
+/*  Widget  */
+.ui-widget-content {
+        border: 1px solid #9e9e9e;
+        border-bottom-color: #b2b2b2;
+}
+
+.ui-widget-content {
+    background: #ffffff;
+    color: #333333;
+}
+
+
+/* Index */
+
+#index {
+    margin: 0;
+    padding: 0;
+    width: 100%;
+    font-style : normal;
+}
+
+#index #frontispiece {
+    margin: auto;
+    padding: 1em;
+    width: 700px;
+}
+
+.booktitle {
+    font-size : 300%; line-height: 100%; font-style:bold;
+    color: white;
+    padding-top: 70px;
+    padding-bottom: 20px; }
+.authors { font-size : 200%;
+           line-height: 115%;  }
+.moreauthors { font-size : 170%  }
+.buttons { font-size : 170%;
+           margin-left: auto;
+           margin-right: auto;
+           font-style : bold;
+         }
+
+/* Link colors never changes */
+
+A:link, A:visited, A:active, A:hover {
+  text-decoration: none;
+  color: #555555
+}
+
+/* Special color for the chapter header */
+
+.booktitleinheader A:visited, .booktitleinheader A:active, .booktitleinheader A:hover, .booktitleinheader A:link {
+  text-decoration: none;
+  color: black;
+}
+
+#index #entrance {
+    text-align: center;
+}
+
+/* This was removed via CSS but the HTML is still generated */
+#index #footer {
+    display: none;
+}
+
+.paragraph {
+    height: 0.6em;
+}
+
+ul.doclist {
+    margin-top: 0em;
+    margin-bottom: 0em;
+}
+
+/* Index styles */
+
+/* Styles the author box (Intro class) and With (column class) */
+
+.column {
+    float:left;
+    width: 43%;
+    margin:0 10px;
+    text-align: left;
+    font-size: 15px;
+    line-height: 25px;
+    padding-right: 20px;
+    min-height: 340px;
+}
+
+.smallauthors {
+    font-size: 19px;
+    line-height: 25px;
+}
+
+.mediumauthors {
+    font-size: 23px;
+    line-height: 33px;
+}
+
+.largeauthors {
+    font-size: 28px;
+    line-height: 40px;
+}
+
+.intro {
+    width: 35%;
+    font-size: 21px;
+    line-height: 27px;
+    font-weight: 600;
+    padding-right: 20px;
+}
+
+.column.pub {
+    width: 40%;
+    margin-bottom: 20px;
+}
+
+#index_content {
+    width: 100%!important;
+    display: block;
+    min-height: 400px;
+}
+
+div.column.pub table tbody tr td {
+    text-align: center; padding: 10px;
+}
+div.column.pub table tbody tr td p {
+    text-align: left;
+    margin-top: 0;
+    font-weight: 600;
+    font-size: 13px!important;
+    line-height: 18px;
+}
+
+/* Tables */
+
+td.tab {
+    height: 16px;
+    font-weight: 600;
+    padding-left: 5px;
+    text-align: left!important;
+}
+
+/* Styles tables on the index -- body class sf_home is used there */
+
+body.sf_home table {
+    min-height: 450px;
+    vertical-align: top;
+}
+
+body.sf_home table td {
+    vertical-align: top;
+
+}
+body.sf_home table td p {
+    min-height: 100px;
+
+}
+
+table.logical { background-color: rgba(144, 160, 209, 0.5);  }
+table.logical tbody tr td.tab { background-color: #91a1d1; }
+
+table.language_found { background-color: rgba(178, 88, 88, 0.5);  }
+table.language_found  tbody tr td.tab { background-color: #b25959; }
+
+table.algo {  background-color: rgba(194, 194, 108, 0.5); }
+table.algo  tbody tr td.tab { background-color: #c2c26c; }
+
+table.qc {  background-color: rgba(185, 170, 185, 0.5); }
+table.qc tbody tr td.tab { background-color: #8b7d95; }
+
+table.vc {  background-color: rgba(159, 125, 140, 0.5); }
+table.vc tbody tr td.tab { background-color: rgb(159, 125, 140); }
+
+table.slf {  background-color: rgba(219, 178, 127, 0.5); }
+table.slf tbody tr td.tab { background-color: rgb(219, 178, 127); }
+
+/* Suggested background color for next volume */
+/*     #c07d62    */
+
+.ui-draggable, .ui-droppable {
+    background-position: top;
+}
+
+/* Chapter dependencies (SVG) */
+.deps a polygon:hover { opacity: 0.6; stroke-width: 2; }
+.deps a text { pointer-events: none; }
+
+/* A few specific things for the top-level SF landing page */
+
+body.sf_home {background-color: #ededed; background-image: url(../media/image/core_mem_bg.jpg); }
+
+body.sf_home #header {
+    background-image: url(../media/image/core_mem_hdr_bg.jpg);
+    padding-bottom: 20px;
+}
+
+body.sf_home #main_home {
+    background-color: transparent;
+}
+
+/* A partial fix to a coqdoc bug...
+   See https://github.com/DeepSpec/sfdev/issues/236 */
+.inlinecode { white-space: pre; }
+.inlinecode br { display: none; }
+
+#header { background-color: rgba(190, 170, 190, 0.5); }
+
+/*   This volume's color   */
+.section, ul#menu li.section_name, div.button  { background-color: #8b7d95; }
+
+.slide img {
+   border: 2px solid gray;
+   margin: 1em;
+}
diff --git a/docs/fdl.org b/docs/res/fdl.org
index 81e2cd9..81e2cd9 100644
--- a/docs/fdl.org
+++ b/docs/res/fdl.org