1 files changed, 37 insertions, 0 deletions
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
new file mode 100644
index 000000000..195ad38c0
--- /dev/null
+++ b/grammar/grammar.mllib
@@ -0,0 +1,37 @@
+Coq_config
+
+Pp_control
+Compat
+Flags
+Pp
+Segmenttree
+Unicodetable
+Errors
+Util
+Bigint
+Hashcons
+Predicate
+Option
+
+Names
+Libnames
+Genarg
+Tok
+Lexer
+Extend
+Extrawit
+Pcoq
+Q_util
+Q_coqast
+Egramml
+Argextend
+Tacextend
+Vernacextend
+
+Redops
+Constrexpr_ops
+Locusops
+G_prim
+G_tactic
+G_ltac
+G_constr