aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/mltop.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/mltop.ml4')
-rw-r--r--toplevel/mltop.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index d1910c145..9bac42c93 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -231,7 +231,7 @@ let stdlib_use_plugins = Coq_config.has_natdynlink
let initial_plugins =
[ "Extraction_plugin"; "Cc_plugin"; "Ground_plugin"; "Dp_plugin";
- "Recdef_plugin"; (*"subtac_plugin";*) "Xml_plugin"; ]
+ "Recdef_plugin"; "Subtac_plugin"; "Xml_plugin"; ]
(** Other plugins of the standard library. We need their list
to avoid trying to load them if they have been statically compiled