From 5da573031d36c5a1df5dcf64cc8764f489f774f7 Mon Sep 17 00:00:00 2001
From: CJ Bell
Date: Thu, 10 Nov 2016 22:28:13 -0500
Subject: Remove unused feedback_content: Goals

---
 lib/feedback.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'lib/feedback.ml')

diff --git a/lib/feedback.ml b/lib/feedback.ml
index 44b3ee35d7..57c6f30a41 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -27,7 +27,6 @@ type feedback_content =
   | ProcessingIn of string
   | InProgress of int
   | WorkerStatus of string * string
-  | Goals of Loc.t * string
   | AddedAxiom
   | GlobRef of Loc.t * string * string * string * string
   | GlobDef of Loc.t * string * string * string
-- 
cgit v1.2.3