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, 2 insertions, 2 deletions
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index caf3d8508..c2dce0231 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -63,13 +63,12 @@ Evd
Reductionops
Inductiveops
Miscops
-Glob_term
+Glob_ops
Detyping
Pattern
Topconstr
Genarg
Ppextend
-Tacops
Tok
Lexer
Extend
@@ -84,6 +83,7 @@ Argextend
Tacextend
Vernacextend
+Redops
G_prim
G_tactic
G_ltac