summaryrefslogtreecommitdiffstats
path: root/site/posts/Ltac101.v
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-02-16 22:35:11 +0100
committerThomas Letan <lthms@soap.coffee>2020-02-16 22:35:11 +0100
commitb47ee36ceab517ba84234bf09e3bb01035450a9a (patch)
tree9d5cad60ba02a7a724f3c660f3b91e781bf0676d /site/posts/Ltac101.v
parent25e6a8c049dbc19ac752dda5995929695a1e10f1 (diff)
Automatically generate a revision table from git history
Diffstat (limited to 'site/posts/Ltac101.v')
-rw-r--r--site/posts/Ltac101.v11
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 *)