7 files changed, 47 insertions, 36 deletions
diff --git a/site/posts/DiscoveringCommonLisp.org b/site/posts/DiscoveringCommonLisp.org
index a198c3d..cf31874 100644
--- a/site/posts/DiscoveringCommonLisp.org
+++ b/site/posts/DiscoveringCommonLisp.org
@@ -1,10 +1,10 @@
 #+BEGIN_EXPORT html
 <h1>Discovering Common Lisp with <code>trivial-gamekit</code></h1>
 
-<span class="time">June 17, 2018</span>
+<p>This article has originally been published on <span class="time">June 17,
+2018</span>.</p>
 #+END_EXPORT
 
-
 I always wanted to learn some Lisp dialect.
 In the meantime, [[https://github.com/lkn-org/lykan][lykan]] —my Slayers Online clone— begins to take shape.
 So, of course, my brain got an idea: /why not writing a client for lykan in some
@@ -30,6 +30,10 @@ gist]].
 #+OPTIONS: toc:nil
 #+TOC: headlines 2
 
+#+BEGIN_EXPORT html
+<div id="history">site/posts/DiscoveringCommonLisp.org</div>
+#+END_EXPORT
+
 * Common Lisp, Quicklisp and trivial-gamekit
 
 The trivial-gamekit [[https://borodust.github.io/projects/trivial-gamekit/][website]] lists several requirements.
diff --git a/site/posts/ExtensibleTypeSafeErrorHandling.org b/site/posts/ExtensibleTypeSafeErrorHandling.org
index 9164bc2..0d40ed7 100644
--- a/site/posts/ExtensibleTypeSafeErrorHandling.org
+++ b/site/posts/ExtensibleTypeSafeErrorHandling.org
@@ -1,12 +1,17 @@
 #+BEGIN_EXPORT html
 <h1>Extensible Type-Safe Error Handling in Haskell</h1>
 
-<span class="time">February 04, 2018</span>
+<p>This article has originally been published on <span class="time">February 04,
+2018</span>.</p>
 #+END_EXPORT
 
 #+OPTIONS: toc:nil
 #+TOC: headlines 2
 
+#+BEGIN_EXPORT html
+<div id="history">site/posts/ExtensibleTypeSafeErrorHandling.org</div>
+#+END_EXPORT
+
 A colleague of mine introduced me to the benefits of [[https://crates.io/crates/error-chain][~error-chain~]], a crate which
 aims to implement /“consistent error handling”/ for Rust. I found the overall
 design pretty convincing, and in his use case, the crate really makes its error
diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v
index ebf3566..61d3bc9 100644
--- a/site/posts/Ltac101.v
+++ b/site/posts/Ltac101.v
@@ -1,15 +1,16 @@
-(** #
-<h1>Ltac 101</h1>
+(** #<h1>Ltac 101</h1>#
 
-<span class="time">October 16, 2017</span>
-    # *)
+    This article has originally been published on #<span class="time">October
+    16, 2017</span>#. *)
 
 (** 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. *)
 
-(** #<div id="generate-toc"></div># *)
+(** #<div id="generate-toc"></div>#
+
+    #<div id="history">site/posts/Ltac101.v</div># *)
 
 (** ** Tactics Aliases *)
 
diff --git a/site/posts/MiniHTTPServer.v b/site/posts/MiniHTTPServer.v
index ee6b572..e944075 100644
--- a/site/posts/MiniHTTPServer.v
+++ b/site/posts/MiniHTTPServer.v
@@ -1,6 +1,7 @@
 (** #<h1>Implementing and Certifying a Web Server in Coq</h1># *)
 
-(** #<span class="time">February 02, 2020</span># *)
+(** This article has originally been published on #<span class="time">February
+02, 2020</span>#. *)
 
 (** FreeSpec is a general-purpose framework for implementing (with a Free monad)
     and certifying (with contracts) impure computations. In this tutorial, we
@@ -11,6 +12,8 @@
 
     #<div id="generate-toc"></div>#
 
+    #<div id="history">site/posts/MiniHTTPServer.v</div>#
+
     The [FreeSpec.Core] module reexports the key component provided by
     FreeSpec. *)
 
diff --git a/site/posts/MonadTransformers.org b/site/posts/MonadTransformers.org
index e94f07d..7947ef4 100644
--- a/site/posts/MonadTransformers.org
+++ b/site/posts/MonadTransformers.org
@@ -1,11 +1,16 @@
 #+BEGIN_EXPORT html
 <h1>Monad Transformers are a Great Abstraction</h1>
 
-<span class="time">July 15, 2017</span>
+<p>This article has originally been published on <span class="time">July 15,
+2017</span>.</p>
 #+END_EXPORT
 
 #+OPTIONS: toc:nil
 
+#+BEGIN_EXPORT html
+<div id="history">site/posts/MonadTransformers.org</div>
+#+END_EXPORT
+
 Monads are hard to get right. I think it took me around a year of Haskelling to
 feel like I understood them. The reason is, to my opinion, there is not such
 thing as /the/ Monad. It is even the contrary. When someone asks me how I would
diff --git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctions.v
index 6564413..3adfe50 100644
--- a/site/posts/StronglySpecifiedFunctions.v
+++ b/site/posts/StronglySpecifiedFunctions.v
@@ -1,13 +1,9 @@
-(** #
-<h1>Strongly-Specified Functions in Coq, part 1: using the <code>refine</code> Tactic</h1>
+(** # <h1>Strongly-Specified Functions in Coq, part 1: using the <code>refine</code> Tactic</h1>#
 
-<p>
-  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="/posts/StronglySpecifiedFunctionsProgram">here</a>.
-</p>
-# *)
+  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="/posts/StronglySpecifiedFunctionsProgram">here</a>#. *)
 
 (** I started to play with Coq, the interactive theorem prover
     developed by Inria, a few weeks ago. It is a very powerful tool,
@@ -23,16 +19,18 @@
     return value is the list passed in argument in which the first
     element has been removed for example.
 
-    But since we will manipulate lists in this article, we first
+    #<div id="generate-toc"></div>#
+
+    #<div id="history">site/posts/StronglySpecifiedFunctions.v</div># *)
+
+(** ** Is this list empty? *)
+
+(** Since we will manipulate lists in this article, we first
     enable several notations of the standard library. *)
 
 From Coq Require Import List.
 Import ListNotations.
 
-(** #<div id="generate-toc"></div># *)
-
-(** ** Is this list empty? *)
-
 (** It's the first question to deal with when manipulating
     lists. There are some functions that require their arguments not
     to be empty. It's the case for the [pop] function, for instance:
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v
index 24faf27..037b0dd 100644
--- a/site/posts/StronglySpecifiedFunctionsProgram.v
+++ b/site/posts/StronglySpecifiedFunctionsProgram.v
@@ -1,18 +1,13 @@
-(** #
-<h1>Strongly-Specified Functions in Coq, part 2: the <code>Program</code> Framework</h1>
+(** #<h1>Strongly-Specified Functions in Coq, part 2: the <code>Program</code> Framework</h1>#
 
-<p>
-  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="/posts/StronglySpecifiedFunctions">here</a>.
-</p>
-# *)
+    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="/posts/StronglySpecifiedFunctions">here</a>#. # *)
 
-(** #<div id="generate-toc"></div># *)
+(** #<div id="generate-toc"></div>#
 
-(** For the past few weeks, I have been playing around with the <<Program>> (or
-    Russel) framework of Coq. *)
+    #<div id="history">site/posts/StronglySpecifiedFunctionsProgram.v</div># *)
 
 (** ** The Theory *)