From 1e8def9c26a169ff344180cdb9c47c5f7f4b216e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 24 Jan 2018 16:28:42 +0100
Subject: Remove dead code from funind.

---
 plugins/funind/recdef.mli | 1 -
 1 file changed, 1 deletion(-)

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

diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 50b84731b5..b95d64ce9e 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,6 +1,5 @@
 open Constr
 
-(* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *)
 val tclUSER_if_not_mes : 
   Tacmach.tactic ->
   bool -> 
-- 
cgit v1.2.3