summaryrefslogtreecommitdiffstats
path: root/site/posts/Ltac101.v
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-07-14 11:26:58 +0200
committerThomas Letan <lthms@soap.coffee>2020-07-14 11:26:58 +0200
commitc62a61dba7285a034fc0405edbd47dcc48bf03f5 (patch)
tree994a21ae6741acb026e73a8d0e85933f04562732 /site/posts/Ltac101.v
parent3deedaa389ab67148e1ca55febf919b30fbb4df2 (diff)
Prepare the introduction of a RSS feed
Diffstat (limited to 'site/posts/Ltac101.v')
-rw-r--r--site/posts/Ltac101.v12
1 files changed, 6 insertions, 6 deletions
diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v
index 1bc9907..bd539e7 100644
--- a/site/posts/Ltac101.v
+++ b/site/posts/Ltac101.v
@@ -1,12 +1,12 @@
(** * Ltac 101
- This article has originally been published on #<span class="time">October
- 16, 2017</span>#. *)
+ This article has . *)
-(** 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. *)
+(** In this article (originally published on #<span
+ id="original-created-at">October 16, 2017</span>#), 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>#