From d2ee641e7fc80918475d5100c92e8119d722e735 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 19 Sep 2020 19:08:35 -0700 Subject: [PATCH] chore: restore macro --- src/Lean/Util/Trace.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index 9f717ae2c3..57d85ef5c9 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -133,6 +133,6 @@ new_frontend namespace Lean --- macro:max "trace!" id:term:max msg:term : term => `(trace $id fun _ => ($msg : MessageData)) +macro:max "trace!" id:term:max msg:term : term => `(trace $id fun _ => ($msg : MessageData)) end Lean