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.mli | 3 ---
 1 file changed, 3 deletions(-)

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

diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index cd5202a6c7..550f727951 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -9,9 +9,6 @@ val mk_correct_id : Id.t -> Id.t
 val mk_complete_id : Id.t -> Id.t
 val mk_equation_id : Id.t -> Id.t
 
-
-val msgnl : Pp.t -> unit
-
 val fresh_id : Id.t list -> string -> Id.t
 val fresh_name : Id.t list -> string -> Name.t
 val get_name : Id.t list -> ?default:string -> Name.t -> Name.t
-- 
cgit v1.2.3