File tree Expand file tree Collapse file tree 2 files changed +2
-0
lines changed
Expand file tree Collapse file tree 2 files changed +2
-0
lines changed Original file line number Diff line number Diff line change @@ -6516,6 +6516,7 @@ public import Mathlib.Tactic.ExistsI
65166516public import Mathlib.Tactic.Explode
65176517public import Mathlib.Tactic.Explode.Datatypes
65186518public import Mathlib.Tactic.Explode.Pretty
6519+ public import Mathlib.Tactic.Ext
65196520public import Mathlib.Tactic.ExtendDoc
65206521public import Mathlib.Tactic.ExtractGoal
65216522public import Mathlib.Tactic.ExtractLets
Original file line number Diff line number Diff line change @@ -85,6 +85,7 @@ public import Mathlib.Tactic.ExistsI
8585public import Mathlib.Tactic.Explode
8686public import Mathlib.Tactic.Explode.Datatypes
8787public import Mathlib.Tactic.Explode.Pretty
88+ public import Mathlib.Tactic.Ext
8889public import Mathlib.Tactic.ExtendDoc
8990public import Mathlib.Tactic.ExtractGoal
9091public import Mathlib.Tactic.ExtractLets
You can’t perform that action at this time.
0 commit comments