From 9fcae6ffe982c9d4f7a38bfef89caaf9e34e966f Mon Sep 17 00:00:00 2001
From: larsk21 <57503246+larsk21@users.noreply.github.com>
Date: Thu, 7 Jul 2022 17:12:34 +0200
Subject: [PATCH] fix: replace `constant` with `opaque`

---
 src/Lean/Linter/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean
index 6550bcaf91..b2d0655552 100644
--- a/src/Lean/Linter/Basic.lean
+++ b/src/Lean/Linter/Basic.lean
@@ -99,7 +99,7 @@ def unusedVariables : Linter := fun stx => do
       isInStructure,
       isInInductive,
       isInCtorOrStructBinder,
-      isInConstantOrAxiom,
+      isInOpaqueOrAxiom,
       isInDefWithForeignDefinition,
       isInDepArrow
     ]
@@ -169,7 +169,7 @@ where
     stackMatches stack [`null, none, `null, ``Lean.Parser.Command.optDeclSig, none] &&
     (stack.get? 4 |>.any fun (stx, _) =>
       [``Lean.Parser.Command.ctor, ``Lean.Parser.Command.structSimpleBinder].any (stx.isOfKind ·))
-  isInConstantOrAxiom (_ : Syntax) (stack : SyntaxStack) :=
+  isInOpaqueOrAxiom (_ : Syntax) (stack : SyntaxStack) :=
     stackMatches stack [`null, none, `null, ``Lean.Parser.Command.declSig, none] &&
     (stack.get? 4 |>.any fun (stx, _) =>
       [``Lean.Parser.Command.opaque, ``Lean.Parser.Command.axiom].any (stx.isOfKind ·))