1 files changed, 5 insertions, 0 deletions
diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib
index fc51e48ae4..af1c7149da 100644
--- a/ltac/ltac.mllib
+++ b/ltac/ltac.mllib
@@ -1,3 +1,6 @@
+Tacarg
+Pptactic
+Pltac
 Taccoerce
 Tacsubst
 Tacenv
@@ -5,6 +8,7 @@ Tactic_debug
 Tacintern
 Tacentries
 Profile_ltac
+Tactic_matching
 Tacinterp
 Evar_tactics
 Tactic_option
@@ -19,4 +23,5 @@ Rewrite
 G_rewrite
 Tauto
 G_eqdecide
+G_tactic
 G_ltac