From 10af47a5790987ee5211bac88c3a16396f30bcb0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 26 Nov 2014 18:41:34 +0100
Subject: Feedback: API cleaned up, documented and made user extensible

---
 lib/flags.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index f95c31d9b8..bcd7c59d7b 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -85,8 +85,6 @@ let coqtop_ui = ref false
 let ide_slave = ref false
 let ideslave_coqtop_flags = ref None
 
-let feedback_goals = ref false
-
 let time = ref false
 
 let raw_print = ref false
-- 
cgit v1.2.3