diff options
author | Thomas Letan <lthms@soap.coffee> | 2021-03-28 00:03:41 +0100 |
---|---|---|
committer | Thomas Letan <lthms@soap.coffee> | 2021-03-28 14:19:29 +0200 |
commit | 495f9db0606b0ed09e6fac59dc32de4cdc8c0087 (patch) | |
tree | 82ea5c5e247c664de247a0f3818f393ffdb00067 /site/posts/CoqffiIntro.org | |
parent | Release of coqffi 1.0.0~beta4 (diff) |
2021 Spring redesign
Diffstat (limited to 'site/posts/CoqffiIntro.org')
-rw-r--r-- | site/posts/CoqffiIntro.org | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/site/posts/CoqffiIntro.org b/site/posts/CoqffiIntro.org index 053826b..411f3cf 100644 --- a/site/posts/CoqffiIntro.org +++ b/site/posts/CoqffiIntro.org @@ -1,6 +1,7 @@ -#+BEGIN_EXPORT html -<h1><code>coqffi</code> in a Nutshell</h1> -#+END_EXPORT +#+TITLE: ~coqffi~ in a Nutshell + +#+SERIES: ./Coqffi.html +#+SERIES_NEXT: ./CoqffiEcho.html For each entry of a ~cmi~ file (a /compiled/ ~mli~ file), ~coqffi~ tries to generate an equivalent (from the extraction mechanism @@ -10,9 +11,8 @@ perspective) Coq definition. In this article, we walk through how Note that we do not dive into the vernacular commands ~coqffi~ generates. They are of no concern for users of ~coqffi~. -#+TOC: headlines 2 - #+BEGIN_EXPORT html +<nav id="generate-toc"></nav> <div id="history">site/posts/CoqffiIntro.org</div> #+END_EXPORT |