From f8cc4d7a38b8df958c47f5169669e3fa97d2d35a Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Mon, 6 Apr 2020 09:30:24 -0500
Subject: [PATCH] Address review nit

---
 theories/proofmode/ltac_tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 04a2ecb30..aa53de890 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1397,7 +1397,7 @@ goal with a [unit → unit] function instead, as expected for
 [string_to_ident_hook]. *)
 Ltac make_string_to_ident_hook string_to_ident :=
   fun s => let x := string_to_ident s in
-        exact (fun (x:unit) => tt).
+        exact (λ (x:unit), tt).
 
 (* [string_to_ident] uses [string_to_ident_hook] to turn [s] into an identifier
 and return it. *)
-- 
GitLab