From 29f358f4072ee4c6530b4c523a1754d4c0723893 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 22 Dec 2023 19:17:09 +0100
Subject: Fix a minor extraction issue

---
 compiler/Extract.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 04ad3b75..3d9f0c22 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -610,7 +610,7 @@ and extract_Lambda (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       ctx xl
   in
   F.pp_print_space fmt ();
-  if !backend = Lean then F.pp_print_string fmt "=>"
+  if !backend = Lean || !backend = Coq then F.pp_print_string fmt "=>"
   else F.pp_print_string fmt "->";
   F.pp_print_space fmt ();
   (* Print the body *)
-- 
cgit v1.2.3