diff options
| author | Thomas Letan <lthms@soap.coffee> | 2020-07-14 11:26:58 +0200 |
|---|---|---|
| committer | Thomas Letan <lthms@soap.coffee> | 2020-07-14 11:26:58 +0200 |
| commit | c62a61dba7285a034fc0405edbd47dcc48bf03f5 (patch) | |
| tree | 994a21ae6741acb026e73a8d0e85933f04562732 /site/posts/Ltac101.v | |
| parent | Identify the creation and last update date from the revisions table (diff) | |
Prepare the introduction of a RSS feed
Diffstat (limited to 'site/posts/Ltac101.v')
| -rw-r--r-- | site/posts/Ltac101.v | 12 |
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># |