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_plugin.mlpack | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/funind/recdef_plugin.mlpack')

diff --git a/plugins/funind/recdef_plugin.mlpack b/plugins/funind/recdef_plugin.mlpack
index 2b443f2a1b..755fa4f879 100644
--- a/plugins/funind/recdef_plugin.mlpack
+++ b/plugins/funind/recdef_plugin.mlpack
@@ -6,5 +6,4 @@ Functional_principles_proofs
 Functional_principles_types
 Invfun
 Indfun
-Merge
 G_indfun
-- 
cgit v1.2.3