diff options
Diffstat (limited to 'site/posts/RewritingInCoq.v')
-rw-r--r-- | site/posts/RewritingInCoq.v | 6 |
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># *) |