“For Fun and Benefit” was not an idiomatic expression

2 files changed, 2 insertions, 2 deletions

diff --git a/site/index.org b/site/index.org
index 6426042..6c7e36d 100644
--- a/site/index.org
+++ b/site/index.org
@@ -40,7 +40,7 @@ machine-checked proofs.
   which construct proof terms later checked by Coq.
 
   1. [[./posts/Ltac101.html][Ltac 101]]
-  1. [[./posts/MixingLtacAndGallina.html][Mixing Ltac and Gallina for Fun and Benefits]]
+  1. [[./posts/MixingLtacAndGallina.html][Mixing Ltac and Gallina for Fun and Profit]]
 
 - [[./posts/RewritingInCoq.html][Rewriting in Coq]] ::
   The ~rewrite~ tactics are really useful, since they are not limited to the Coq
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