summaryrefslogtreecommitdiffstats
path: root/site/posts/MixingLtacAndGallina.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/MixingLtacAndGallina.v
parentc0364ffe4ba5bd7cbad88b1792449ee9eb7aa58c (diff)
Make the two articles about Ltac refer to each otherHEADmaster
Diffstat (limited to 'site/posts/MixingLtacAndGallina.v')
-rw-r--r--site/posts/MixingLtacAndGallina.v6
1 files changed, 5 insertions, 1 deletions
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