.gitignore

*.glob
*.d
*.d.raw
*.vio
*.vo
*.cm*
*.annot
*.spit
*.spot
*.o
*.a
*.pyc
*.log
*.aux
*.dvi
*.pdf
*.blg
*.bbl
*.idx
*.ilg
*.toc
*.atoc
*.comidx
*.comind
*.erridx
*.errind
*.haux
*.hcomind
*.herrind
*.hind
*.htacind
*.htoc
*.ind
*.lof
*.tacidx
*.tacind
*.v.tex
*.v.ps
*.v.timing
*.v.timing.diff
*.v.before-timing
*.v.after-timing
*.v.html
*.stamp
*.native
revision
TAGS
.DS_Store
.pc
bin/
_build_ci
_build
config/Makefile
config/coq_config.ml
config/coq_config.py
config/Info-*.plist
dev/ocamldebug-coq
plugins/micromega/csdpcert
plugins/micromega/.micromega.ml.generated
kernel/byterun/dllcoqrun.so
coqdoc.sty
coqdoc.css
time-of-build.log
time-of-build-pretty.log
time-of-build-before.log
time-of-build-after.log
time-of-build-pretty.log2
time-of-build-pretty.log3
.csdp.cache
test-suite/.lia.cache
test-suite/.nra.cache
test-suite/.nia.cache
test-suite/trace
test-suite/misc/universes/all_stdlib.v
test-suite/misc/universes/universes.txt
test-suite/coq-makefile/*/actual
test-suite/coq-makefile/*/desired
test-suite/coq-makefile/**/*.processed
test-suite/coq-makefile/**/Makefile
test-suite/coq-makefile/**/Makefile.conf
test-suite/coq-makefile/*/src
test-suite/coq-makefile/*/theories
test-suite/coq-makefile/*/theories2
test-suite/coq-makefile/*/html
test-suite/coq-makefile/*/mlihtml
test-suite/coq-makefile/*/subdir/done
test-suite/coq-makefile/merlin1/.merlin
test-suite/coqdoc/Coqdoc.*
test-suite/coqdoc/index.html
test-suite/coqdoc/coqdoc.css
test-suite/output/MExtraction.out
test-suite/oUnit-anon.cache
test-suite/unit-tests/**/*.test

# documentation

doc/common/version.tex
doc/faq/html/
doc/faq/axioms.eps
doc/faq/axioms.eps_t
doc/faq/axioms.pdf_t
doc/faq/axioms.png
doc/sphinx/index.rst
doc/sphinx/zebibliography.rst
doc/stdlib/Library.out
doc/stdlib/Library.ps
doc/stdlib/Library.coqdoc.tex
doc/stdlib/FullLibrary.ps
doc/stdlib/FullLibrary.coqdoc.tex
doc/stdlib/html/
doc/stdlib/index-body.html
doc/stdlib/index-list.html
doc/tools/docgram/productionlistGrammar
doc/tools/docgram/editedGrammar
doc/tools/docgram/prodnGrammar
doc/tutorial/Tutorial.v.out
doc/RecTutorial/RecTutorial.html
doc/RecTutorial/RecTutorial.ps

# .mll files

coqpp/coqpp_lex.ml
dev/ocamlweb-doc/lex.ml
ide/coq_lex.ml
ide/config_lexer.ml
ide/utf8_convert.ml
tools/coqwc.ml
tools/coqdep_lexer.ml
tools/ocamllibdep.ml
tools/coqdoc/cpretty.ml
ide/protocol/xml_lexer.ml

# .mly files

coqpp/coqpp_parse.ml
coqpp/coqpp_parse.mli

# .ml4 / .mlp files

g_*.ml

plugins/ltac/coretactics.ml
plugins/ltac/extratactics.ml
plugins/ltac/extraargs.ml
plugins/ltac/profile_ltac_tactics.ml
ide/coqide_os_specific.ml
plugins/ssrmatching/ssrmatching.ml
plugins/ssr/ssrparser.ml
plugins/ssr/ssrvernac.ml

# other auto-generated files

kernel/byterun/coq_instruct.h
kernel/byterun/coq_jumptbl.h
kernel/genOpcodeFiles.exe
kernel/copcodes.ml
kernel/uint63.ml
ide/default.bindings
ide/default_bindings_src.exe
ide/index_urls.txt
.lia.cache
.nia.cache

# emacs save files
*~
\#*\#

# coqide generated files (when testing)
*.crashcoqide

/user-contrib/*
!/user-contrib/Ltac2

.*.sw*
.#*

plugins/ssr/ssrparser.ml
plugins/ssr/ssrvernac.ml

/gramlib/.pack

# ocaml dev files
.merlin
META.coq

# Files automatically generated by Dune.
plugins/*/dune
theories/*/dune
theories/*/*/dune
theories/*/*/*/dune
/user-contrib/Ltac2/dune
*.install
!Makefile.install

ide/coqide.keys