From 0508f7b0fba0582c38129a2787965c99a15eb1c7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 15 Jul 2019 10:06:38 +0200
Subject: [funind] Removed dead code.

---
 plugins/funind/indfun_common.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'plugins/funind/indfun_common.ml')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 80fc64fe65..b55d8537d6 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -10,8 +10,6 @@ let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
 let mk_complete_id id = Nameops.add_suffix (mk_rel_id id) "_complete"
 let mk_equation_id id = Nameops.add_suffix id "_equation"
 
-let msgnl m = ()
-
 let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) (Id.Set.of_list avoid)
 
 let fresh_name avoid s = Name (fresh_id avoid s)
-- 
cgit v1.2.3