diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index 27a8181..57712a3 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -184,22 +184,6 @@ elab "TacticDoc" name:ident content:str : command =>
     name := name.getId,
     content := content.getString })
 
-/-- Declare a set of tactic documentation entries.
-Expect an identifier used as the set name then `:=` and a
-space separated list of identifiers.
--/
-elab "TacticSet" name:ident ":=" args:ident* : command => do
-  let docs := tacticDocExt.getState (← getEnv)
-  let mut entries : Array TacticDocEntry := #[]
-  for arg in args do
-    let name := arg.getId
-    match docs.find? (·.name = name) with
-    | some doc => entries := entries.push doc
-    | none => throwError "Documentation for tactic {name} wasn't found."
-  modifyEnv (tacticSetExt.addEntry · {
-    name := name.getId,
-    tactics := entries })
-
 instance : Quote TacticDocEntry `term :=
 ⟨λ entry => Syntax.mkCApp ``TacticDocEntry.mk #[quote entry.name, quote entry.content]⟩
 
@@ -209,15 +193,12 @@ entry or a tactic doc set. -/
 elab "Tactics" args:ident* : command => do
   let env ← getEnv
   let docs := tacticDocExt.getState env
-  let sets := tacticSetExt.getState env
   let mut tactics : Array TacticDocEntry := #[]
   for arg in args do
     let name := arg.getId
     match docs.find? (·.name = name) with
     | some entry => tactics := tactics.push entry
-    | none => match sets.find? (·.name = name) with
-              | some entry => tactics := tactics ++ entry.tactics
-              | none => throwError "Tactic doc or tactic set {name} wasn't found."
+    | none => throwError "Tactic doc {name} wasn't found."
   modifyCurLevel fun level => pure {level with tactics := tactics}
 
 /-! ## Lemmas -/
diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean
index c4e97c6..fb4ab8a 100644
--- a/server/leanserver/GameServer/EnvExtensions.lean
+++ b/server/leanserver/GameServer/EnvExtensions.lean
@@ -45,25 +45,6 @@ elab "#print_tactic_doc" : command => do
   for entry in tacticDocExt.getState (← getEnv) do
     dbg_trace "{entry.name} : {entry.content}"
 
-structure TacticSetEntry where
-  name : Name
-  tactics : Array TacticDocEntry
-  deriving ToJson, Repr
-
-/-- Environment extension for tactic sets. -/
-initialize tacticSetExt : SimplePersistentEnvExtension TacticSetEntry (Array TacticSetEntry) ←
-  registerSimplePersistentEnvExtension {
-    name := `tactic_set
-    addEntryFn := Array.push
-    addImportedFn := Array.concatMap id
-  }
-
-open Elab Command in
-/-- Print all registered tactic sets for debugging purposes. -/
-elab "#print_tactic_set" : command => do
-  for entry in tacticSetExt.getState (← getEnv) do
-    dbg_trace "{entry.name} : {entry.tactics.map TacticDocEntry.name}"
-
 /-! ## Lemma documentation -/
 
 structure LemmaDocEntry where