summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-02-16 22:45:51 +0100
committerThomas Letan <lthms@soap.coffee>2020-02-16 22:45:51 +0100
commit3b79b7e6ae441c92e9f97abd1532ac0dd34fe068 (patch)
tree311b543fce325dd2fe83c9ad18138f938b5397d5
parentb47ee36ceab517ba84234bf09e3bb01035450a9a (diff)
Add a revision table to the “Rewrite in Coq” article
-rw-r--r--site/posts/RewritingInCoq.v11
1 files changed, 6 insertions, 5 deletions
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 *)