From f080389c3f5572dda0f768f0ddf66d5eae82a9b0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 5 Mar 2021 10:28:57 -0800
Subject: [PATCH] chore: use double-backtick

---
 src/Lean/Elab/Inductive.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index fac27e4aae..41d848db67 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -430,10 +430,10 @@ private def applyInferMod (views : Array InductiveView) (numParams : Nat) (indTy
 
 private def mkAuxConstructions (views : Array InductiveView) : TermElabM Unit := do
   let env ← getEnv
-  let hasEq   := env.contains `Eq
-  let hasHEq  := env.contains `HEq
-  let hasUnit := env.contains `PUnit
-  let hasProd := env.contains `Prod
+  let hasEq   := env.contains ``Eq
+  let hasHEq  := env.contains ``HEq
+  let hasUnit := env.contains ``PUnit
+  let hasProd := env.contains ``Prod
   for view in views do
     let n := view.declName
     mkRecOn n