1 files changed, 1 insertions, 0 deletions
diff --git a/_tags b/_tags
index d236caee..69df3480 100644
--- a/_tags
+++ b/_tags
@@ -55,6 +55,7 @@
 "tactics/rewrite.ml4": use_grammar
 
 <plugins/**/*.ml4>: use_grammar
+"plugins/subtac/g_subtac.ml4": use_extend
 
 ## sub-directory inclusion