From e75daed95ad1c92af4e577fea95e234d7a8401c1 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 29 Aug 2023 14:49:46 -0700 Subject: [PATCH] Import delaborator from other files. This makes doc-gen use the Q(...) syntax. --- Qq/MetaM.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Qq/MetaM.lean b/Qq/MetaM.lean index 7611df8..a3f399c 100644 --- a/Qq/MetaM.lean +++ b/Qq/MetaM.lean @@ -1,4 +1,5 @@ import Qq.Macro +import Qq.Delab open Lean Elab Term Meta