summaryrefslogtreecommitdiffstats
path: root/site/posts/MixingLtacAndGallina.v
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-07-31 09:17:57 +0200
committerThomas Letan <lthms@soap.coffee>2020-07-31 09:17:57 +0200
commitc0364ffe4ba5bd7cbad88b1792449ee9eb7aa58c (patch)
tree0d978a6dbe6979ea79979c6d6032b3216b5fa31d /site/posts/MixingLtacAndGallina.v
parentf25464afcc3c7ab8e3164f011552b1245af31a84 (diff)
“For Fun and Benefit” was not an idiomatic expression
Diffstat (limited to 'site/posts/MixingLtacAndGallina.v')
-rw-r--r--site/posts/MixingLtacAndGallina.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/site/posts/MixingLtacAndGallina.v b/site/posts/MixingLtacAndGallina.v
index fb30186..adebb3a 100644
--- a/site/posts/MixingLtacAndGallina.v
+++ b/site/posts/MixingLtacAndGallina.v
@@ -1,4 +1,4 @@
-(** * Mixing Ltac and Gallina for Fun and Benefits *)
+(** * Mixing Ltac and Gallina for Fun and Profit *)
(** 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