-
+
+October 16, 2017
# *)
(** In this article, I give an overview of my findings about the Ltac language,
diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v
index 5ebf6c6..542190c 100644
--- a/site/posts/RewritingInCoq.v
+++ b/site/posts/RewritingInCoq.v
@@ -1,6 +1,7 @@
(** #
Rewriting in Coq
-
+
+May 13, 2017
# *)
(** I have to confess something. In the published codebase of SpecCert lies a
diff --git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctions.v
index 9aceb67..d241c26 100644
--- a/site/posts/StronglySpecifiedFunctions.v
+++ b/site/posts/StronglySpecifiedFunctions.v
@@ -1,6 +1,7 @@
(** #
Strongly-Specified Functions in Coq with the refine Tactic
-
+
+January 11, 2015
# *)
(** I started to play with Coq, the interactive theorem prover
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v
index 78ccefb..122a9ef 100644
--- a/site/posts/StronglySpecifiedFunctionsProgram.v
+++ b/site/posts/StronglySpecifiedFunctionsProgram.v
@@ -1,12 +1,10 @@
(** #
Strongly-Specified Functions in Coq with the Program Framework
+# *)
-
-This blogpost was initially published on , and as later been heavily rewritten in
-late 2019.
-
- # *)
+(** This blogpost was initially published on #
+ January 01, 2017#, and as later been heavily rewritten in
+ late 2019. *)
(** ## *)
diff --git a/site/posts/extensible-type-safe-error-handling.org b/site/posts/extensible-type-safe-error-handling.org
index 115b3e8..9164bc2 100644
--- a/site/posts/extensible-type-safe-error-handling.org
+++ b/site/posts/extensible-type-safe-error-handling.org
@@ -1,6 +1,7 @@
#+BEGIN_EXPORT html
If you like what you read, have a question or for any other reasons really,
diff --git a/site/posts/lisp-journey-getting-started.org b/site/posts/lisp-journey-getting-started.org
index 3d8a6c1..a198c3d 100644
--- a/site/posts/lisp-journey-getting-started.org
+++ b/site/posts/lisp-journey-getting-started.org
@@ -1,6 +1,7 @@
#+BEGIN_EXPORT html