diff options
author | Thomas Letan <lthms@soap.coffee> | 2020-02-16 22:35:11 +0100 |
---|---|---|
committer | Thomas Letan <lthms@soap.coffee> | 2020-02-16 22:35:11 +0100 |
commit | b47ee36ceab517ba84234bf09e3bb01035450a9a (patch) | |
tree | 9d5cad60ba02a7a724f3c660f3b91e781bf0676d /site/posts/Ltac101.v | |
parent | Add a dedicated icon for GitHub links (diff) |
Automatically generate a revision table from git history
Diffstat (limited to 'site/posts/Ltac101.v')
-rw-r--r-- | site/posts/Ltac101.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v index ebf3566..61d3bc9 100644 --- a/site/posts/Ltac101.v +++ b/site/posts/Ltac101.v @@ -1,15 +1,16 @@ -(** # -<h1>Ltac 101</h1> +(** #<h1>Ltac 101</h1># -<span class="time">October 16, 2017</span> - # *) + This article has originally been published on #<span class="time">October + 16, 2017</span>#. *) (** In this article, I give an overview of my findings about the Ltac language, more precisely how it can be used to automate the construction of proof terms. If you never wrote a tactic in Coq and are curious about the subject, it might be a good starting point. *) -(** #<div id="generate-toc"></div># *) +(** #<div id="generate-toc"></div># + + #<div id="history">site/posts/Ltac101.v</div># *) (** ** Tactics Aliases *) |