aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/grammar.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/grammar.mllib')
-rw-r--r--parsing/grammar.mllib6
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index 4356db844..0c815d262 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -1,7 +1,7 @@
Coq_config
Profile
-Pp_control
+Pp_control
Pp
Compat
Flags
@@ -49,7 +49,7 @@ Nametab
Libobject
Lib
Goptions
-Decl_kinds
+Decl_kinds
Global
Termops
Evd
@@ -68,7 +68,7 @@ Vernacexpr
Extrawit
Pcoq
Q_util
-Q_coqast
+Q_coqast
Egrammar
Argextend