diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /parsing/grammar.mllib | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'parsing/grammar.mllib')
-rw-r--r-- | parsing/grammar.mllib | 88 |
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 |