chore: remove unnecessary 'open'; compatibility with v4.11.0-rc3 (#54)

leanprover-community · Aug 29, 2024 · d38fb94 · d38fb94
1 parent 71f5442
commit d38fb94
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Qq/Macro.lean b/Qq/Macro.lean
@@ -9,7 +9,7 @@ This file provides the main feature of `Qq`; the `q( )` and `Q( )` macros,
 which are available with `open scoped Qq`.
 -/
 
-open Lean Meta Std
+open Lean Meta
 
 namespace Qq