From c2bb9b043bee85e390f4c59d52cb97a489faf85d Mon Sep 17 00:00:00 2001
From: Thomas Letan <lthms@soap.coffee>
Date: Fri, 31 Jul 2020 09:18:47 +0200
Subject: Make the two articles about Ltac refer to each other

---
 site/posts/Ltac101.v              | 14 +++++++++-----
 site/posts/MixingLtacAndGallina.v |  6 +++++-
 2 files changed, 14 insertions(+), 6 deletions(-)

(limited to 'site')

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>#
 
diff --git a/site/posts/MixingLtacAndGallina.v b/site/posts/MixingLtacAndGallina.v
index adebb3a..1fd1228 100644
--- a/site/posts/MixingLtacAndGallina.v
+++ b/site/posts/MixingLtacAndGallina.v
@@ -1,6 +1,10 @@
 (** * Mixing Ltac and Gallina for Fun and Profit *)
 
-(** One of the most misleading introduction to Coq is to say that “Gallina is
+(** This write-up is the second part of a series on Ltac, the default tactic
+    language of Coq. The first part explains #<a href="/posts/Ltac101.html">how
+    Coq users can define their own tactics</a>#.
+
+    One of the most misleading introduction to Coq is to say that “Gallina is
     for programs, while tactics are for proofs.”  Indeed, in Coq we construct
     terms of given types, always. Terms encodes both programs and proofs about
     these programs. Gallina is the preferred way to construct programs, and
-- 
cgit v1.2.3