aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/grammar.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/grammar.mllib')
-rw-r--r--parsing/grammar.mllib4
1 files changed, 3 insertions, 1 deletions
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index 128ca9445..9e714352b 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -64,10 +64,12 @@ Tacexpr
Lexer
Extend
Vernacexpr
+Extrawit
Pcoq
Q_util
Q_coqast
+Egrammar
Argextend
Tacextend
Vernacextend
@@ -75,4 +77,4 @@ Vernacextend
G_prim
G_tactic
G_ltac
-G_constr \ No newline at end of file
+G_constr