diff options
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 *) |