summaryrefslogtreecommitdiff
path: root/grammar/grammar.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'grammar/grammar.mllib')
-rw-r--r--grammar/grammar.mllib65
1 files changed, 0 insertions, 65 deletions
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
deleted file mode 100644
index 71e5b8ae..00000000
--- a/grammar/grammar.mllib
+++ /dev/null
@@ -1,65 +0,0 @@
-Coq_config
-
-Hook
-Terminal
-Canary
-Hashset
-Hashcons
-CSet
-CMap
-Int
-HMap
-Option
-Store
-Exninfo
-Backtrace
-Pp_control
-Flags
-Loc
-CList
-CString
-Serialize
-Stateid
-Feedback
-Pp
-
-CArray
-CStack
-Util
-Ppstyle
-Errors
-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