fix

leanprover-community · Feb 13, 2024 · 82be4b4 · 82be4b4
1 parent 0bf1cdc
commit 82be4b4
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean
@@ -47,11 +47,11 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
     if args.hasFlag "exclude-meta" then
       -- Mathlib-specific exclusion of tactics
       let filterMathlibMeta : Name → Bool := fun n => (
-        isPrefixOf `Mathlib.Lean.Tactic n ∨
+        isPrefixOf `Mathlib.Tactic n ∨
         isPrefixOf `Mathlib.Lean n ∨
-        isPrefixOf `Mathlib.Lean.Mathport n ∨
-        isPrefixOf `Mathlib.Lean.Util n)
-      graph := graph.filterGraph filterMathlibMeta (replacement := `«Mathlib.Lean.Tactics»)
+        isPrefixOf `Mathlib.Mathport n ∨
+        isPrefixOf `Mathlib.Util n)
+      graph := graph.filterGraph filterMathlibMeta (replacement := `«Mathlib.Tactics»)
     if args.hasFlag "reduce" then
       graph := graph.transitiveReduction
     return asDotGraph graph