From 3b79b7e6ae441c92e9f97abd1532ac0dd34fe068 Mon Sep 17 00:00:00 2001
From: Thomas Letan <lthms@soap.coffee>
Date: Sun, 16 Feb 2020 22:45:51 +0100
Subject: =?UTF-8?q?Add=20a=20revision=20table=20to=20the=20=E2=80=9CRewrit?=
 =?UTF-8?q?e=20in=20Coq=E2=80=9D=20article?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 site/posts/RewritingInCoq.v | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'site/posts')

diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v
index 542190c..390df90 100644
--- a/site/posts/RewritingInCoq.v
+++ b/site/posts/RewritingInCoq.v
@@ -1,8 +1,7 @@
-(** #
-<h1>Rewriting in Coq</h1>
+(** #<h1>Rewriting in Coq</h1>#
 
-<span class="time">May 13, 2017</span>
-    # *)
+    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
@@ -14,7 +13,9 @@
     term in a proof using a ad-hoc equivalence relation and, when
     necessary, a proper morphism. *)
 
-(** #<div id="generate-toc"></div># *)
+(** #<div id="generate-toc"></div>#
+
+    #<div id="history">site/posts/RewritingInCoq.v</div># *)
 
 (** ** Gate: Our Case Study *)
 
-- 
cgit v1.2.3