diff options
Diffstat (limited to 'site/posts/MixingLtacAndGallina.v')
| -rw-r--r-- | site/posts/MixingLtacAndGallina.v | 5 |
1 files changed, 4 insertions, 1 deletions
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># *) |