From 8acbb55632c774b5ccb89b99da818716f6a65c26 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Aug 2021 14:05:00 -0700 Subject: [PATCH] chore: fix tests --- tests/lean/Reformat.lean | 2 +- tests/lean/run/Reparen.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/Reformat.lean b/tests/lean/Reformat.lean index 53f4310398..0961b736ce 100644 --- a/tests/lean/Reformat.lean +++ b/tests/lean/Reformat.lean @@ -1,5 +1,5 @@ -/-! Parse and reformat file -/ import Lean.PrettyPrinter +/-! Parse and reformat file -/ open Lean open Lean.Elab diff --git a/tests/lean/run/Reparen.lean b/tests/lean/run/Reparen.lean index d1e12cc4a9..2098c8499e 100644 --- a/tests/lean/run/Reparen.lean +++ b/tests/lean/run/Reparen.lean @@ -1,5 +1,5 @@ -/-! Reprint file after removing all parentheses and then passing it through the parenthesizer -/ import Lean.Parser +/-! Reprint file after removing all parentheses and then passing it through the parenthesizer -/ open Lean open Std.Format open Std