diff options
| author | Thomas Letan <lthms@soap.coffee> | 2020-02-16 22:45:51 +0100 |
|---|---|---|
| committer | Thomas Letan <lthms@soap.coffee> | 2020-02-16 22:45:51 +0100 |
| commit | 3b79b7e6ae441c92e9f97abd1532ac0dd34fe068 (patch) | |
| tree | 311b543fce325dd2fe83c9ad18138f938b5397d5 /site/posts/RewritingInCoq.v | |
| parent | Automatically generate a revision table from git history (diff) | |
Add a revision table to the “Rewrite in Coq” article
Diffstat (limited to 'site/posts/RewritingInCoq.v')
| -rw-r--r-- | site/posts/RewritingInCoq.v | 11 |
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 *) |