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 -
 lib/feedback.mli | 1 -
 2 files changed, 2 deletions(-)

(limited to 'lib')

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
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 5160bd5bc1..b4bed8793d 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -36,7 +36,6 @@ type feedback_content =
   | InProgress of int
   | WorkerStatus of string * string
   (* Generally useful metadata *)
-  | 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