Verified Commit f8cc4d7a authored by Tej Chajed's avatar Tej Chajed

Address review nit

parent 7e33ffcb
...@@ -1397,7 +1397,7 @@ goal with a [unit → unit] function instead, as expected for ...@@ -1397,7 +1397,7 @@ goal with a [unit → unit] function instead, as expected for
[string_to_ident_hook]. *) [string_to_ident_hook]. *)
Ltac make_string_to_ident_hook string_to_ident := Ltac make_string_to_ident_hook string_to_ident :=
fun s => let x := string_to_ident s in 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 (* [string_to_ident] uses [string_to_ident_hook] to turn [s] into an identifier
and return it. *) and return it. *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment