From 495f9db0606b0ed09e6fac59dc32de4cdc8c0087 Mon Sep 17 00:00:00 2001
From: Thomas Letan <lthms@soap.coffee>
Date: Sun, 28 Mar 2021 00:03:41 +0100
Subject: 2021 Spring redesign

---
 site/posts/MixingLtacAndGallina.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'site/posts/MixingLtacAndGallina.v')

diff --git a/site/posts/MixingLtacAndGallina.v b/site/posts/MixingLtacAndGallina.v
index 4e6b28d..d77cd8a 100644
--- a/site/posts/MixingLtacAndGallina.v
+++ b/site/posts/MixingLtacAndGallina.v
@@ -1,3 +1,6 @@
+(** #<nav><p class="series">Ltac.html</p>
+     <p class="series-prev">./LtacPatternMatching.html</p></nav># *)
+
 (** * Mixing Ltac and Gallina for Fun and Profit *)
 
 (** One of the most misleading introduction to Coq is to say that “Gallina is
@@ -20,7 +23,7 @@
     It turns out these features are more than handy when it comes to
     metaprogramming (that is, the generation of programs by programs). *)
 
-(** #<div id="generate-toc"></div>#
+(** #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/MixingLtacAndGallina.v</div># *)
 
-- 
cgit v1.2.3