From 35f683e2d8c1ff031e52e397efeb9bc0a74d83dd Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 25 Feb 2025 23:15:32 +0000 Subject: [PATCH] Actually import the new file (#72) This was a mistake in #71. --- Qq.lean | 3 ++- Qq/Simp.lean | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Qq.lean b/Qq.lean index 41b60d4..015d918 100644 --- a/Qq.lean +++ b/Qq.lean @@ -1,5 +1,6 @@ import Qq.Macro import Qq.Delab import Qq.MetaM +import Qq.Simp import Qq.Match -import Qq.AssertInstancesCommute \ No newline at end of file +import Qq.AssertInstancesCommute diff --git a/Qq/Simp.lean b/Qq/Simp.lean index 84f825f..617986e 100644 --- a/Qq/Simp.lean +++ b/Qq/Simp.lean @@ -1,4 +1,4 @@ -import Mathlib.Util.Qq +import Qq.MetaM /-! # Qq integration for `simproc`s