8 files changed, 36 insertions, 37 deletions
diff --git a/site/posts/CleopatraV1.org b/site/posts/CleopatraV1.org
index 349e237..11d796b 100644
--- a/site/posts/CleopatraV1.org
+++ b/site/posts/CleopatraV1.org
@@ -28,6 +28,10 @@ purpose is to introduce two Makefiles: ~Makefile~ and ~bootstrap.mk~.
 
 #+TOC: headlines 2
 
+#+BEGIN_EXPORT html
+<div id="history">site/posts/CleopatraV1.org</div>
+#+END_EXPORT
+
 ~Makefile~ serves two purposes: it initiates a few global variables, and it
 provides a rule to generate ~bootstrap.mk~.  At this point, some readers may
 wonder /why/ we need ~Makefile~ in this context, and the motivation behind this
diff --git a/site/posts/ClightIntroduction.v b/site/posts/ClightIntroduction.v
index 0d53f33..13bf773 100644
--- a/site/posts/ClightIntroduction.v
+++ b/site/posts/ClightIntroduction.v
@@ -8,10 +8,9 @@ Import ListNotations.
     you write is preserved by CompCert compilation passes up to the generated
     machine code.
 
-    I have been interested in CompCert for quite some times now. Today (#<span
-    id="time">#March 18, 2020#</span>#), I have challenged myself to study
-    Clight and its semantics. This write-up is the result of this challenge,
-    written as I was progressing.
+    I had been interested in CompCert for quite some times, and ultimately
+    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>#
 
diff --git a/site/posts/ExtensibleTypeSafeErrorHandling.org b/site/posts/ExtensibleTypeSafeErrorHandling.org
index 3af3d44..cc276f0 100644
--- a/site/posts/ExtensibleTypeSafeErrorHandling.org
+++ b/site/posts/ExtensibleTypeSafeErrorHandling.org
@@ -1,8 +1,8 @@
 #+BEGIN_EXPORT html
 <h1>Extensible Type-Safe Error Handling in Haskell</h1>
 
-<p>This article has originally been published on <span class="time">February 04,
-2018</span>.</p>
+<p>This article has originally been published on <span
+id="original-created-at">February 04, 2018</span>.</p>
 #+END_EXPORT
 
 #+TOC: headlines 2
diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v
index 1bc9907..bd539e7 100644
--- a/site/posts/Ltac101.v
+++ b/site/posts/Ltac101.v
@@ -1,12 +1,12 @@
 (** * Ltac 101
 
-    This article has originally been published on #<span class="time">October
-    16, 2017</span>#. *)
+    This article has . *)
 
-(** In this article, I give an overview of my findings about the Ltac language,
-    more precisely how it can be used to automate the construction of proof
-    terms. If you never wrote a tactic in Coq and are curious about the subject,
-    it might be a good starting point. *)
+(** In this article (originally published on #<span
+    id="original-created-at">October 16, 2017</span>#), I give an overview of my
+    findings about the Ltac language, more precisely how it can be used to
+    automate the construction of proof terms. If you never wrote a tactic in Coq
+    and are curious about the subject, it might be a good starting point. *)
 
 (** #<div id="generate-toc"></div>#
 
diff --git a/site/posts/MonadTransformers.org b/site/posts/MonadTransformers.org
index 4c28fe5..b2bd2ca 100644
--- a/site/posts/MonadTransformers.org
+++ b/site/posts/MonadTransformers.org
@@ -1,8 +1,8 @@
 #+BEGIN_EXPORT html
 <h1>Monad Transformers are a Great Abstraction</h1>
 
-<p>This article has originally been published on <span class="time">July 15,
-2017</span>.</p>
+<p>This article has originally been published on <span
+id="original-created-at">July 15, 2017</span>.</p>
 #+END_EXPORT
 
 #+OPTIONS: toc:nil
diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v
index 9c2efaf..0020a3e 100644
--- a/site/posts/RewritingInCoq.v
+++ b/site/posts/RewritingInCoq.v
@@ -1,17 +1,13 @@
-(** * Rewriting in Coq
-
-    This article has originally been published on #<span class="time">May 13,
-    2017</span>.# *)
-
-(** I have to confess something. In the published codebase of SpecCert lies a
-    shameful secret. It takes the form of a set of axioms which are not
-    required. I thought they were when I wrote them, but it was before I heard
-    about “generalized rewriting,” setoids and morphisms.
-
-    Now, I know the truth. I will have to update SpecCert eventually. But,
-    in the meantime, let me try to explain how it is possible to rewrite a
-    term in a proof using a ad-hoc equivalence relation and, when
-    necessary, a proper morphism. *)
+(** * Rewriting in Coq *)
+
+(** I have to confess something. In the codebase of SpecCert lies a shameful
+    secret. It takes the form of a set of unnecessary axioms. I thought I
+    couldn’t avoid them at first, but it was before I heard about “generalized
+    rewriting,” setoids and morphisms.  Now, I know the truth, and I will have
+    to update SpecCert eventually. But, in the meantime, let me try to explain
+    in this article originally published on #<span id="original-created-at">May
+    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>#
 
diff --git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctions.v
index ac55b7e..5d0e69a 100644
--- a/site/posts/StronglySpecifiedFunctions.v
+++ b/site/posts/StronglySpecifiedFunctions.v
@@ -1,11 +1,11 @@
-(** * Strongly-Specified Functions in Coq, part 1: using the <<refine>> Tactic
+(** * Strongly-Specified Functions in Coq, part 1: using the <<refine>> Tactic *)
 
-    This is the first article (initially published on #<span
-    class="time">January 11, 2015</span>#) of a series of two on how to write
-    strongly-specified functions in Coq. You can read the next part #<a
-    href="./StronglySpecifiedFunctionsProgram.html">here</a>#. *)
+(** This is the first article (initially published on #<span
+    class="original-created-at">January 11, 2015</span>#) of a series of two on
+    how to write strongly-specified functions in Coq. You can read the next part
+    #<a href="./StronglySpecifiedFunctionsProgram.html">here</a>#.
 
-(** I started to play with Coq, the interactive theorem prover
+    I started to play with Coq, the interactive theorem prover
     developed by Inria, a few weeks ago. It is a very powerful tool,
     yet hard to master. Fortunately, there are some very good readings
     if you want to learn (I recommend the Coq'Art). This article is
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v
index 2a998aa..f7f84df 100644
--- a/site/posts/StronglySpecifiedFunctionsProgram.v
+++ b/site/posts/StronglySpecifiedFunctionsProgram.v
@@ -1,9 +1,9 @@
 (** * Strongly-Specified Functions in Coq, part 2: the <<Program>> Framework
 
     This is the second article (initially published on #<span
-    class="time">January 01, 2017</span>#) of a series of two on how to write
-    strongly-specified functions in Coq. You can read the previous part #<a
-    href="./StronglySpecifiedFunctions.html">here</a>#. # *)
+    id="original-created-at">January 01, 2017</span>#) of a series of two on how
+    to write strongly-specified functions in Coq. You can read the previous part
+    #<a href="./StronglySpecifiedFunctions.html">here</a>#. # *)
 
 (** #<div id="generate-toc"></div>#