aboutsummaryrefslogtreecommitdiff
path: root/plugins/decl_mode
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/decl_mode')
-rw-r--r--plugins/decl_mode/decl_mode_plugin.mllib1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/decl_mode/decl_mode_plugin.mllib b/plugins/decl_mode/decl_mode_plugin.mllib
index dce989bbcd..39342dbd1c 100644
--- a/plugins/decl_mode/decl_mode_plugin.mllib
+++ b/plugins/decl_mode/decl_mode_plugin.mllib
@@ -1,4 +1,3 @@
-Decl_expr
Decl_mode
Decl_interp
Decl_proof_instr