From b8cf967b841d54b0efdb03d28b0f2d4512389c24 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 4 Dec 2021 22:32:34 +0100
Subject: [PATCH] chore: Focus on basic declarations for now

---
 DocGen4/Process.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index 9e5924e..0aefa85 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -64,7 +64,6 @@ inductive DocInfo where
 | inductiveInfo (info : InductiveInfo) : DocInfo
 | structureInfo (info : StructureInfo) : DocInfo
 | classInfo (info : ClassInfo) : DocInfo
-| classInductiveInfo : DocInfo
 
 structure Module where
   name : Name