summaryrefslogtreecommitdiffstats
path: root/site/posts/RewritingInCoq.v
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2021-03-28 00:03:41 +0100
committerThomas Letan <lthms@soap.coffee>2021-03-28 14:19:29 +0200
commit495f9db0606b0ed09e6fac59dc32de4cdc8c0087 (patch)
tree82ea5c5e247c664de247a0f3818f393ffdb00067 /site/posts/RewritingInCoq.v
parent1a197fb354a82a31deca4f9b118f057bbd0038b6 (diff)
2021 Spring redesign
Diffstat (limited to 'site/posts/RewritingInCoq.v')
-rw-r--r--site/posts/RewritingInCoq.v6
1 files changed, 5 insertions, 1 deletions
diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v
index 0020a3e..a285e09 100644
--- a/site/posts/RewritingInCoq.v
+++ b/site/posts/RewritingInCoq.v
@@ -1,3 +1,7 @@
+(** #<nav><p class="series">../coq.html</p>
+ <p class="series-prev">./Ltac.html</p>
+ <p class="series-next">./ClightIntroduction.html</p></nav># *)
+
(** * Rewriting in Coq *)
(** I have to confess something. In the codebase of SpecCert lies a shameful
@@ -9,7 +13,7 @@
13, 2017</span> how it is possible to rewrite a term in a proof using a
ad-hoc equivalence relation and, when necessary, a proper morphism. *)
-(** #<div id="generate-toc"></div>#
+(** #<nav id="generate-toc"></nav>#
#<div id="history">site/posts/RewritingInCoq.v</div># *)