summaryrefslogtreecommitdiff
path: root/plugins/decl_mode/decl_mode_plugin.mlpack
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/decl_mode/decl_mode_plugin.mlpack')
-rw-r--r--plugins/decl_mode/decl_mode_plugin.mlpack5
1 files changed, 0 insertions, 5 deletions
diff --git a/plugins/decl_mode/decl_mode_plugin.mlpack b/plugins/decl_mode/decl_mode_plugin.mlpack
deleted file mode 100644
index 1b84a079..00000000
--- a/plugins/decl_mode/decl_mode_plugin.mlpack
+++ /dev/null
@@ -1,5 +0,0 @@
-Decl_mode
-Decl_interp
-Decl_proof_instr
-Ppdecl_proof
-G_decl_mode