summaryrefslogtreecommitdiff
path: root/parsing/grammar.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/grammar.mllib')
-rw-r--r--parsing/grammar.mllib88
1 files changed, 0 insertions, 88 deletions
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
deleted file mode 100644
index ba393e63..00000000
--- a/parsing/grammar.mllib
+++ /dev/null
@@ -1,88 +0,0 @@
-Coq_config
-
-Profile
-Pp_control
-Pp
-Compat
-Flags
-Segmenttree
-Unicodetable
-Util
-Errors
-Bigint
-Dyn
-Hashcons
-Predicate
-Rtree
-Option
-Store
-Hashtbl_alt
-
-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
-Glob_term
-Detyping
-Pattern
-Topconstr
-Genarg
-Ppextend
-Tacexpr
-Tok
-Lexer
-Extend
-Vernacexpr
-Extrawit
-Pcoq
-Q_util
-Q_coqast
-
-Egrammar
-Argextend
-Tacextend
-Vernacextend
-
-G_prim
-G_tactic
-G_ltac
-G_constr