From c0364ffe4ba5bd7cbad88b1792449ee9eb7aa58c Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Fri, 31 Jul 2020 09:17:57 +0200 Subject: =?UTF-8?q?=E2=80=9CFor=20Fun=20and=20Benefit=E2=80=9D=20was=20not?= =?UTF-8?q?=20an=20idiomatic=20expression?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- site/posts/MixingLtacAndGallina.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'site/posts') 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 -- cgit v1.2.3