From 3f657326c3b68eeea7f16aeaf06dc5ff8fdd61c4 Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Fri, 20 Aug 2021 11:35:45 +0200 Subject: Fix a Coq warning --- site/posts/CoqffiEcho.org | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'site/posts/CoqffiEcho.org') diff --git a/site/posts/CoqffiEcho.org b/site/posts/CoqffiEcho.org index b9c531e..8d48c48 100644 --- a/site/posts/CoqffiEcho.org +++ b/site/posts/CoqffiEcho.org @@ -333,7 +333,7 @@ typeclass. #+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v Notation "'let_rec*' f x ':=' p 'in' q" := (let f := mfix (fun f x => p) in q) - (at level 61, x pattern, f ident, q at next level, right associativity). + (at level 61, x pattern, f name, q at next level, right associativity). #+END_SRC Note that ~mfix~ does /not/ check whether or not the defined function -- cgit v1.2.3