summaryrefslogtreecommitdiff
path: root/grammar/grammar.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'grammar/grammar.mllib')
-rw-r--r--grammar/grammar.mllib62
1 files changed, 62 insertions, 0 deletions
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
new file mode 100644
index 00000000..0b168377
--- /dev/null
+++ b/grammar/grammar.mllib
@@ -0,0 +1,62 @@
+Coq_config
+
+Hook
+Canary
+Hashset
+Hashcons
+CSet
+CMap
+Int
+HMap
+Option
+Store
+Exninfo
+Backtrace
+Pp_control
+Flags
+Loc
+Serialize
+Stateid
+Feedback
+Pp
+Errors
+CList
+CString
+CArray
+CStack
+Util
+Bigint
+Predicate
+Segmenttree
+Unicodetable
+Unicode
+Genarg
+
+Evar
+Names
+
+Libnames
+
+Redops
+Miscops
+Locusops
+
+Stdarg
+Constrarg
+Constrexpr_ops
+
+Compat
+Tok
+Lexer
+Pcoq
+G_prim
+G_tactic
+G_ltac
+G_constr
+
+Q_util
+Q_coqast
+Egramml
+Argextend
+Tacextend
+Vernacextend