From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 4 Jun 2012 12:07:52 +0200
Subject: Imported Upstream version 8.4~gamma0+really8.4beta2

---
 proofs/refiner.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'proofs/refiner.ml')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 5cd85547..8901a5a2 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -415,10 +415,6 @@ let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
 let pp_info = ref (fun _ _ _ -> assert false)
 let set_info_printer f = pp_info := f
 
-let tclINFO (tac : tactic) gls =
-  msgnl (hov 0 (str "Warning: info is currently not working"));
-  tac gls
-
 (* Check that holes in arguments have been resolved *)
 
 let check_evars env sigma extsigma gl =
-- 
cgit v1.2.3