1 files changed, 84 insertions, 0 deletions
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
new file mode 100644
index 00000000..248a8ad9
--- /dev/null
+++ b/parsing/grammar.mllib
@@ -0,0 +1,84 @@
+Coq_config
+
+Profile
+Pp_control
+Pp
+Compat
+Flags
+Segmenttree
+Unicodetable
+Util
+Bigint
+Dyn
+Hashcons
+Predicate
+Rtree
+Option
+
+Names
+Univ
+Esubst
+Term
+Mod_subst
+Sign
+Cbytecodes
+Copcodes
+Cemitcodes
+Declarations
+Retroknowledge
+Pre_env
+Cbytegen
+Environ
+Conv_oracle
+Closure
+Reduction
+Type_errors
+Entries
+Modops
+Inductive
+Typeops
+Indtypes
+Cooking
+Term_typing
+Subtyping
+Mod_typing
+Safe_typing
+
+Nameops
+Libnames
+Summary
+Nametab
+Libobject
+Lib
+Goptions
+Decl_kinds
+Global
+Termops
+Namegen
+Evd
+Reductionops
+Inductiveops
+Rawterm
+Detyping
+Pattern
+Topconstr
+Genarg
+Ppextend
+Tacexpr
+Lexer
+Extend
+Vernacexpr
+Extrawit
+Pcoq
+Q_util
+Q_coqast
+
+Egrammar
+Argextend
+Tacextend
+Vernacextend
+
+G_prim
+G_tactic
+G_ltac
+G_constr