summaryrefslogtreecommitdiff
path: root/plugins/funind/recdef_plugin.mlpack
diff options
context:
space:
mode:
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 2b443f2a..755fa4f8 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