aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/recdef_plugin.mlpack
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-24 16:28:42 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-24 17:13:27 +0100
commit1e8def9c26a169ff344180cdb9c47c5f7f4b216e (patch)
treed26bffcbfe899787d85b29db900b5de843630e14 /plugins/funind/recdef_plugin.mlpack
parent2e798fb83db743ce44350af6f7f9442811f374ad (diff)
Remove dead code from funind.
Diffstat (limited to 'plugins/funind/recdef_plugin.mlpack')
-rw-r--r--plugins/funind/recdef_plugin.mlpack1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/funind/recdef_plugin.mlpack b/plugins/funind/recdef_plugin.mlpack
index 2b443f2a1..755fa4f87 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