diff --git a/PhiCalculus.lean b/PhiCalculus.lean
index 68324a34..345f8b83 100644
--- a/PhiCalculus.lean
+++ b/PhiCalculus.lean
@@ -1,6 +1,6 @@
 import Minimal.ARS
 import Minimal.Calculus
--- import Std.Tactic.Lint
+import Std.Tactic.Lint
 
 -- these are all Std linters except docBlame and docBlameThm
--- #lint only checkType checkUnivs defLemma dupNamespace explicitVarsOfIff impossibleInstance nonClassInstance simpComm simpNF simpVarHead synTaut unusedArguments unusedHavesSuffices in Minimal
+#lint only checkType checkUnivs defLemma dupNamespace explicitVarsOfIff impossibleInstance nonClassInstance simpComm simpNF simpVarHead synTaut unusedArguments unusedHavesSuffices in Minimal