15 files changed, 91 insertions, 77 deletions
diff --git a/site/posts/AlgebraicDatatypes.v b/site/posts/AlgebraicDatatypes.v
index 1b24520..f32551c 100644
--- a/site/posts/AlgebraicDatatypes.v
+++ b/site/posts/AlgebraicDatatypes.v
@@ -1,3 +1,7 @@
+(** #<nav><p class="series">../coq.html</p>
+     <p class="series-prev">./ClightIntroduction.html</p>
+     <p class="series-next">./Coqffi.html</p></nav># *)
+
 (** * Proving Algebraic Datatypes are “Algebraic” *)
 
 (** Several programming languages allow programmers to define (potentially
@@ -93,7 +97,7 @@ Inductive prod (A B : Type) : Type :=
 | pair : A -> B -> prod A B
 >>
 
-    #<div id="generate-toc"></div>#
+    #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/AlgebraicDatatypes.v</div># *)
 
diff --git a/site/posts/ClightIntroduction.v b/site/posts/ClightIntroduction.v
index 4bd9a52..85d084b 100644
--- a/site/posts/ClightIntroduction.v
+++ b/site/posts/ClightIntroduction.v
@@ -1,3 +1,7 @@
+(** #<nav><p class="series">../coq.html</p>
+     <p class="series-prev">./RewritingInCoq.html</p>
+     <p class="series-next">./AlgebraicDatatypes.html</p></nav># *)
+
 (** * A Study of Clight and its Semantics *)
 (* begin hide *)
 From Coq Require Import List.
@@ -12,7 +16,7 @@ Import ListNotations.
     challenged myself to study Clight and its semantics. This write-up is the
     result of this challenge, written as I was progressing.
 
-    #<div id="generate-toc"></div>#
+    #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/ClightIntroduction.v</div># *)
 
diff --git a/site/posts/Coqffi.org b/site/posts/Coqffi.org
index 3d8b867..f8d9695 100644
--- a/site/posts/Coqffi.org
+++ b/site/posts/Coqffi.org
@@ -1,6 +1,7 @@
-#+BEGIN_EXPORT html
-<h1>A Series on <code>coqffi</code></h1>
-#+END_EXPORT
+#+TITLE: A series on ~coqffi~
+
+#+SERIES: ../coq.html
+#+SERIES_PREV: AlgebraicDatatypes.html
 
 ~coqffi~ generates Coq FFI modules from compiled OCaml interface
 modules (~.cmi~). In practice, it greatly reduces the hassle to mix
diff --git a/site/posts/CoqffiEcho.org b/site/posts/CoqffiEcho.org
index 04fa253..81ae0e9 100644
--- a/site/posts/CoqffiEcho.org
+++ b/site/posts/CoqffiEcho.org
@@ -1,6 +1,7 @@
-#+BEGIN_EXPORT html
-<h1>Implementing an Echo Server in Coq with <code>coqffi</code></h1>
-#+END_EXPORT
+#+TITLE: Implementing an Echo Server in Coq with ~coqffi~
+
+#+SERIES: ./Coqffi.html
+#+SERIES_PREV: ./CoqffiIntro.html
 
 #+NAME: coqffi_output
 #+BEGIN_SRC sh :results output :exports none :var mod=""
@@ -21,9 +22,8 @@ Besides, this article is a literate program, and you can download
 [[/files/coqffi-tutorial.tar.gz][the resulting source tree]] if you
 want to try to read the source directly, or modify it to your taste.
 
-#+TOC: headlines 2
-
 #+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
 <div id="history">site/posts/CoqffiEcho.org</div>
 #+END_EXPORT
 
diff --git a/site/posts/CoqffiIntro.org b/site/posts/CoqffiIntro.org
index 053826b..411f3cf 100644
--- a/site/posts/CoqffiIntro.org
+++ b/site/posts/CoqffiIntro.org
@@ -1,6 +1,7 @@
-#+BEGIN_EXPORT html
-<h1><code>coqffi</code> in a Nutshell</h1>
-#+END_EXPORT
+#+TITLE: ~coqffi~ in a Nutshell
+
+#+SERIES: ./Coqffi.html
+#+SERIES_NEXT: ./CoqffiEcho.html
 
 For each entry of a ~cmi~ file (a /compiled/ ~mli~ file), ~coqffi~
 tries to generate an equivalent (from the extraction mechanism
@@ -10,9 +11,8 @@ perspective) Coq definition. In this article, we walk through how
 Note that we do not dive into the vernacular commands ~coqffi~
 generates. They are of no concern for users of ~coqffi~.
 
-#+TOC: headlines 2
-
 #+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
 <div id="history">site/posts/CoqffiIntro.org</div>
 #+END_EXPORT
 
diff --git a/site/posts/ExtensibleTypeSafeErrorHandling.org b/site/posts/ExtensibleTypeSafeErrorHandling.org
index cc276f0..e817e31 100644
--- a/site/posts/ExtensibleTypeSafeErrorHandling.org
+++ b/site/posts/ExtensibleTypeSafeErrorHandling.org
@@ -1,13 +1,14 @@
-#+BEGIN_EXPORT html
-<h1>Extensible Type-Safe Error Handling in Haskell</h1>
+#+TITLE: Extensible Type-Safe Error Handling in Haskell
+
+#+SERIES: ../haskell.html
 
+#+BEGIN_EXPORT html
 <p>This article has originally been published on <span
 id="original-created-at">February 04, 2018</span>.</p>
 #+END_EXPORT
 
-#+TOC: headlines 2
-
 #+BEGIN_EXPORT html
+<nav id="generate-toc"></nav>
 <div id="history">site/posts/ExtensibleTypeSafeErrorHandling.org</div>
 #+END_EXPORT
 
diff --git a/site/posts/Ltac.org b/site/posts/Ltac.org
index caba76c..37580cd 100644
--- a/site/posts/Ltac.org
+++ b/site/posts/Ltac.org
@@ -1,12 +1,16 @@
-#+BEGIN_EXPORT html
-<h1>A Series on Ltac</h1>
-#+END_EXPORT
+#+TITLE: A Series on Ltac
+
+#+SERIES: ../coq.html
+#+SERIES_PREV: ./StronglySpecifiedFunctions.html
+#+SERIES_NEXT: ./RewritingInCoq.html
 
 Ltac is the “tactic language” of Coq. It is commonly advertised as the common
-approach to write proofs, which tends to bias how it is introduced to new Coq
-users (/e.g./, in Master courses). In this series, we present Ltac as the
-metaprogramming tool it is, since fundamentally it is an imperative language
-which allows for constructing Coq terms interactively and incrementally.
+approach to write proofs, which tends to bias how it is introduced to
+new Coq users[fn::I know /I/ was introduced to Coq in a similar way in
+my Master courses.]. In this series, we present Ltac as the
+metaprogramming tool it is, since fundamentally it is an imperative
+language which allows for constructing Coq terms interactively and
+incrementally.
 
 - [[./LtacMetaprogramming.html][Ltac is an Imperative Metaprogramming Language]] ::
   Ltac generates terms, therefore it is a metaprogramming language. It does it
diff --git a/site/posts/LtacMetaprogramming.v b/site/posts/LtacMetaprogramming.v
index 2a4fe50..6b086e3 100644
--- a/site/posts/LtacMetaprogramming.v
+++ b/site/posts/LtacMetaprogramming.v
@@ -1,3 +1,6 @@
+(** #<nav><p class="series">Ltac.html</p>
+     <p class="series-next">LtacPatternMatching.html</p></nav># *)
+
 (** * Ltac is an Imperative Metaprogramming Language *)
 
 (** #<div id="history">site/posts/LtacMetaprogramming.v</div># *)
diff --git a/site/posts/LtacPatternMatching.v b/site/posts/LtacPatternMatching.v
index d52d0bf..a0b8a4d 100644
--- a/site/posts/LtacPatternMatching.v
+++ b/site/posts/LtacPatternMatching.v
@@ -1,3 +1,7 @@
+(** #<nav><p class="series">Ltac.html</p>
+     <p class="series-prev">./LtacMetaprogramming.html</p>
+     <p class="series-next">./MixingLtacAndGallina.html</p></nav># *)
+
 (** * Pattern Matching on Types and Contexts  *)
 
 (** In the #<a href="LtacMetaprogramming.html">#previous article#</a># of our
@@ -11,7 +15,7 @@
     contexts. In this article, we give a short introduction on this feature of
     key importance. *)
 
-(** #<div id="generate-toc"></div>#
+(** #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/LtacPatternMatching.v</div># *)
 
@@ -137,8 +141,8 @@ Ltac not_param_type x :=
   | _ => idtac
   end.
 
-(** Both <<not_param_type (@nil nat)>> of type [list nat] and <<(@eq_refl nat
-    0)>> of type [0 = 0] fail, but <<not_param_type 0>> of type [nat]
+(** Both <<not_param_type (@nil nat)>> of type [list nat] and
+    <<(@eq_refl nat 0)>> of type [0 = 0] fail, but <<not_param_type 0>> of type [nat]
     succeeds. *)
 
 (** ** Pattern Matching on the Context with [goal] *)
diff --git a/site/posts/MixingLtacAndGallina.v b/site/posts/MixingLtacAndGallina.v
index 4e6b28d..d77cd8a 100644
--- a/site/posts/MixingLtacAndGallina.v
+++ b/site/posts/MixingLtacAndGallina.v
@@ -1,3 +1,6 @@
+(** #<nav><p class="series">Ltac.html</p>
+     <p class="series-prev">./LtacPatternMatching.html</p></nav># *)
+
 (** * Mixing Ltac and Gallina for Fun and Profit *)
 
 (** One of the most misleading introduction to Coq is to say that “Gallina is
@@ -20,7 +23,7 @@
     It turns out these features are more than handy when it comes to
     metaprogramming (that is, the generation of programs by programs). *)
 
-(** #<div id="generate-toc"></div>#
+(** #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/MixingLtacAndGallina.v</div># *)
 
diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v
index 0020a3e..a285e09 100644
--- a/site/posts/RewritingInCoq.v
+++ b/site/posts/RewritingInCoq.v
@@ -1,3 +1,7 @@
+(** #<nav><p class="series">../coq.html</p>
+     <p class="series-prev">./Ltac.html</p>
+     <p class="series-next">./ClightIntroduction.html</p></nav># *)
+
 (** * Rewriting in Coq *)
 
 (** I have to confess something. In the codebase of SpecCert lies a shameful
@@ -9,7 +13,7 @@
     13, 2017</span> how it is possible to rewrite a term in a proof using a
     ad-hoc equivalence relation and, when necessary, a proper morphism. *)
 
-(** #<div id="generate-toc"></div>#
+(** #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/RewritingInCoq.v</div># *)
 
diff --git a/site/posts/StronglySpecifiedFunctions.org b/site/posts/StronglySpecifiedFunctions.org
index 805b944..83148c6 100644
--- a/site/posts/StronglySpecifiedFunctions.org
+++ b/site/posts/StronglySpecifiedFunctions.org
@@ -1,8 +1,7 @@
-#+OPTIONS: toc:nil num:nil
+#+TITLE: A Series on Strongly-Specified Functions in Coq
 
-#+BEGIN_EXPORT html
-<h1>A Series on Strongly-Specified Functions in Coq</h1>
-#+END_EXPORT
+#+SERIES: ../coq.html
+#+SERIES_NEXT: ./Ltac.html
 
 Using dependent types and the ~Prop~ sort, it becomes possible to specify
 functions whose arguments and results are constrained by properties.  Using such
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v
index 1b4ab5f..c5763ea 100644
--- a/site/posts/StronglySpecifiedFunctionsProgram.v
+++ b/site/posts/StronglySpecifiedFunctionsProgram.v
@@ -5,7 +5,7 @@
     to write strongly-specified functions in Coq. You can read the previous part
     #<a href="./StronglySpecifiedFunctionsRefine.html">here</a>#. # *)
 
-(** #<div id="generate-toc"></div>#
+(** #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/StronglySpecifiedFunctionsProgram.v</div># *)
 
@@ -341,7 +341,8 @@ Defined.
 (** val extract : 'a1 vector -> nat -> nat -> 'a1 vector **)
 let extract v e b =
   take (drop v b) (sub e b)
->> *)
+>>
+    *)
 
 (** I was pretty happy, so I tried some more. Each time, using [nth], I managed
     to write a precise post condition and to prove it holds true. For instance,
@@ -467,7 +468,8 @@ cannot be applied to the terms
  "b" : "Type"
 The 3rd term has type "Type" which should be coercible
 to "nat".
->> *)
+>>
+    *)
 
 #[program]
 Fixpoint map2 {a b c n}
@@ -520,4 +522,5 @@ cannot be applied to the terms
  "wildcard'" : "vector A n'"
 The 3rd term has type "vector A n'" which should be
 coercible to "nat".
->> *)
+>>
+    *)
diff --git a/site/posts/StronglySpecifiedFunctionsRefine.v b/site/posts/StronglySpecifiedFunctionsRefine.v
index 1d4ec2e..4ffb385 100644
--- a/site/posts/StronglySpecifiedFunctionsRefine.v
+++ b/site/posts/StronglySpecifiedFunctionsRefine.v
@@ -19,7 +19,7 @@
     return value is the list passed in argument in which the first
     element has been removed for example.
 
-    #<div id="generate-toc"></div>#
+    #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/StronglySpecifiedFunctionsRefine.v</div># *)
 
@@ -54,7 +54,8 @@ Import ListNotations.
 <<
 Definition predicate_b (args) :=
   if predicate_dec args then true else false.
->> *)
+>>
+    *)
 
 (** *** Defining the <<empty>> predicate *)
 
@@ -174,7 +175,8 @@ Definition pop {a} (l : list a) (h : ~ empty l)
   h : ~ empty l
   ============================
   list a
->> *)
+>>
+    *)
 
 (** Using the [refine] tactic naively, for instance this way:  *)
 
@@ -280,7 +282,8 @@ Definition pop {a} (l : list a | ~ empty l)
   equ : proj1_sig l = []
   ============================
   {l' : list a | exists a0 : a, proj1_sig l = a0 :: l'}
->> *)
+>>
+    *)
 
   + destruct l as [l nempty]; cbn in *.
     rewrite equ in nempty.
@@ -299,7 +302,8 @@ Definition pop {a} (l : list a | ~ empty l)
   equ : proj1_sig l = a0 :: rst
   ============================
   exists a1 : a, proj1_sig l = a1 :: rst
->> *)
+>>
+    *)
 
   + destruct l as [l nempty]; cbn in *.
     rewrite equ.
@@ -339,7 +343,8 @@ Definition push {a} (l : list a) (x : a)
 <<
 let push l a =
   Cons (a, l)
->> *)
+>>
+    *)
 
 (** ** Defining [head] *)
 
@@ -376,7 +381,8 @@ Defined.
 let head = function
 | Nil -> assert false (* absurd case *)
 | Cons (a, l0) -> a
->> *)
+>>
+    *)
 
 (** ** Conclusion & Moving Forward *)
 
diff --git a/site/posts/Thanks.org b/site/posts/Thanks.org
index ba76a88..c20f1e5 100644
--- a/site/posts/Thanks.org
+++ b/site/posts/Thanks.org
@@ -1,18 +1,15 @@
-#+BEGIN_EXPORT html
-<h1>Thanks!</h1>
-
-<article class="index">
-#+END_EXPORT
+#+TITLE: Thanks!
 
-This website could not exist without (many) awesome free software
-projects. Although I could not list them all even if I wanted, my desire is at
-least to try keeping up-to-date a curated description of the “main” ones.
+#+SERIES: ../meta.html
+#+SERIES_NEXT: ../cleopatra.html
 
-#+OPTIONS: toc:nil num:nil
+This website could not exist without many awesome free software
+projects. Although I could not list them all even if I wanted, my
+desire is at least to try keeping up-to-date a curated description of
+the most significant ones.
 
 #+BEGIN_EXPORT html
-<div id="generate-toc"></div>
-
+<nav id="generate-toc"></nav>
 <div id="history">site/posts/Thanks.org</div>
 #+END_EXPORT
 
@@ -35,9 +32,6 @@ least to try keeping up-to-date a curated description of the “main” ones.
 - [[https://soupault.neocities.org][soupault]] ::
   Soupault is a static website generator and HTML processor written by [[https://www.baturin.org/][Daniil
   Baturin]].
-- [[https://github.com/sass/sassc][~sassc~]] ::
-  ~sassc~ is a compiler for SASS files (actually, a wrapper around [[https://github.com/sass/libsass][~libsass~]]),
-  authored by [[https://github.com/akhleung][Aaron Leung]], [[https://github.com/hcatlin][Hampton Catlin]], [[https://github.com/mgreter][Marcel Greter]], and [[https://github.com/xzyfer][Michael Mifsud]].
 - [[https://cleopatra.soap.coffee][~cleopatra~]] ::
   ~cleopatra~ is a generic, extensible toolchain with facilities for
   literate programming projects using Org mode and more. I have
@@ -45,25 +39,9 @@ least to try keeping up-to-date a curated description of the “main” ones.
 
 * Frontend
 
-- [[https://forkaweso.me/Fork-Awesome/][Fork Awesome]] ::
-  Fork Awesome is a collection of icons for the web. It is a community fork of
-  [[https://fontawesome.com/][Font Awesome]].
 - [[https://katex.org][\im \KaTeX \mi]] ::
   \im \KaTeX \mi is the “fastest” math typesetting library for the web, and is
-  uses to render inline mathematics in my posts at build time. It has been
+  used to render inline mathematics in my posts at build time. It has been
   created by [[https://github.com/xymostech][Emily Eisenberg]] and
   [[https://sophiebits.com/][Sophie Alpert]], with the help of
   [[https://github.com/KaTeX/KaTeX/graphs/contributors][many contributors]].
-- [[https://github.com/tonsky/FiraCode][Fira Code]] ::
-  Fira Code is a monospaced font by [[https://github.com/tonsky][Nikita Prokopov]] inspired with Fira Mono by
-  the [[https://www.mozilla.org/en-US/][Mozilla Foundation]], with “programming ligatures” (/e.g./, =>>==, ====,
-  =!==, etc.), and it is used here for verbatim content (principally source
-  code).
-- [[https://github.com/productiontype/spectral][Spectral]] ::
-  Spectral is an original typeface designed by Production Type,
-  primarily intended for use inside Google’s Docs and Slides.  It is
-  used as the main font of this website.
-
-#+BEGIN_EXPORT html
-</article>
-#+END_EXPORT