aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/ltac_plugin.mlpack
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/ltac_plugin.mlpack')
-rw-r--r--plugins/ltac/ltac_plugin.mlpack4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index 12b4c81fc..3972b7aac 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -1,9 +1,9 @@
Tacarg
+Tacsubst
+Tacenv
Pptactic
Pltac
Taccoerce
-Tacsubst
-Tacenv
Tactic_debug
Tacintern
Tacentries