diff options
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 *) |