summaryrefslogtreecommitdiffstats
path: root/site/posts/Ltac101.v
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-07-31 09:18:47 +0200
committerThomas Letan <lthms@soap.coffee>2020-07-31 09:18:47 +0200
commitc2bb9b043bee85e390f4c59d52cb97a489faf85d (patch)
tree6ce16f196359980cb820605c0042b3377d876f54 /site/posts/Ltac101.v
parentc0364ffe4ba5bd7cbad88b1792449ee9eb7aa58c (diff)
Make the two articles about Ltac refer to each otherHEADmaster
Diffstat (limited to 'site/posts/Ltac101.v')
-rw-r--r--site/posts/Ltac101.v14
1 files changed, 9 insertions, 5 deletions
diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v
index b0841e9..2b71a8f 100644
--- a/site/posts/Ltac101.v
+++ b/site/posts/Ltac101.v
@@ -1,10 +1,14 @@
(** * Ltac 101 *)
-(** 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. *)
+(** We 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.
+
+ This write-up (originally published on #<span
+ id="original-created-at">October 16, 2017</span>#) is the first part of a
+ series on Ltac. The next part explains #<a
+ href="/posts/MixingLtacAndGallina.html">how to mix Gallina and Ltac</a>#. *)
(** #<div id="generate-toc"></div>#