From 9b028566ecaf2db33d0470024df82ab3211a7cce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 16 Apr 2023 09:54:48 +0200 Subject: [PATCH] fix: get rid off deleted attribute --- DocGen4/Process/Attributes.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/DocGen4/Process/Attributes.lean b/DocGen4/Process/Attributes.lean index 307d677..4eccced 100644 --- a/DocGen4/Process/Attributes.lean +++ b/DocGen4/Process/Attributes.lean @@ -52,8 +52,8 @@ abbrev ParametricAttrWrapper := ValueAttrWrapper ParametricAttribute The list of all tag based attributes doc-gen knows about and can recover. -/ def tagAttributes : Array TagAttribute := - #[IR.UnboxResult.unboxAttr, neverExtractAttr, Elab.Term.elabWithoutExpectedTypeAttr, - SynthInstance.inferTCGoalsRLAttr, matchPatternAttr] + #[IR.UnboxResult.unboxAttr, neverExtractAttr, + Elab.Term.elabWithoutExpectedTypeAttr, matchPatternAttr] deriving instance Repr for Compiler.InlineAttributeKind deriving instance Repr for Compiler.SpecializeAttributeKind