summaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore138
1 files changed, 106 insertions, 32 deletions
diff --git a/.gitignore b/.gitignore
index 031b06b5..7fcd2580 100644
--- a/.gitignore
+++ b/.gitignore
@@ -29,49 +29,35 @@
*.htoc
*.ind
*.lof
-*.stamp
*.tacidx
*.tacind
*.v.tex
*.v.pdf
*.v.ps
*.v.html
+*.stamp
revision
TAGS
+.DS_Store
+.pc
bin/
+_build
+plugins/*/*_mod.ml
+myocamlbuild_config.ml
config/Makefile
config/coq_config.ml
-plugins/dp/dp_zenon.ml
dev/ocamldebug-coq
-dev/ocamlweb-doc/lex.ml
-dev/ocamlweb-doc/syntax.ml
-dev/ocamlweb-doc/syntax.mli
-ide/config_lexer.ml
-ide/config_parser.ml
-ide/config_parser.mli
-ide/coq_lex.ml
-ide/extract_index.ml
-ide/find_phrase.ml
-ide/highlight.ml
-ide/undo.mli
-ide/utf8_convert.ml
-kernel/byterun/coq_jumptbl.h
+plugins/micromega/csdpcert
kernel/byterun/dllcoqrun.so
-kernel/copcodes.ml
-scripts/tolink.ml
states/initial.coq
+coqdoc.sty
test-suite/lia.cache
test-suite/trace
-theories/Numbers/Natural/BigN/NMake_gen.v
-tools/coqdep_lexer.ml
-tools/coqdoc/cpretty.ml
-tools/coqwc.ml
-tools/gallina_lexer.ml
-toplevel/mltop.optml
-plugins/micromega/csdpcert
-toplevel/mltop.byteml
-coqdoc.sty
-ide/index_urls.txt
+test-suite/misc/universes/all_stdlib.v
+test-suite/misc/universes/universes.txt
+
+# documentation
+
doc/faq/html/
doc/refman/csdp.cache
doc/refman/trace
@@ -100,8 +86,96 @@ doc/RecTutorial/RecTutorial.html
doc/RecTutorial/RecTutorial.pdf
doc/RecTutorial/RecTutorial.ps
dev/doc/naming-conventions.pdf
-_build
-plugins/*/*_mod.ml
-myocamlbuild_config.ml
-.DS_Store
-.pc
+
+# .mll files
+
+dev/ocamlweb-doc/lex.ml
+ide/coq_lex.ml
+ide/config_lexer.ml
+ide/utf8_convert.ml
+ide/highlight.ml
+plugins/dp/dp_zenon.ml
+tools/gallina_lexer.ml
+tools/coqwc.ml
+tools/coqdep_lexer.ml
+tools/coqdoc/cpretty.ml
+lib/xml_lexer.ml
+
+# .mly files
+
+ide/config_parser.ml
+ide/config_parser.mli
+
+# .ml4 files
+
+ide/project_file.ml
+lib/pp.ml
+lib/compat.ml
+parsing/g_xml.ml
+parsing/g_prim.ml
+parsing/q_util.ml
+parsing/tacextend.ml
+parsing/q_constr.ml
+parsing/g_vernac.ml
+parsing/pcoq.ml
+parsing/g_constr.ml
+parsing/g_ltac.ml
+parsing/vernacextend.ml
+parsing/g_tactic.ml
+parsing/argextend.ml
+parsing/g_decl_mode.ml
+parsing/q_coqast.ml
+parsing/g_proofs.ml
+parsing/lexer.ml
+plugins/xml/proofTree2Xml.ml
+plugins/xml/acic2Xml.ml
+plugins/xml/xml.ml
+plugins/xml/dumptree.ml
+plugins/xml/xmlentries.ml
+plugins/extraction/g_extraction.ml
+plugins/rtauto/g_rtauto.ml
+plugins/romega/g_romega.ml
+plugins/setoid_ring/newring.ml
+plugins/firstorder/g_ground.ml
+plugins/dp/g_dp.ml
+plugins/cc/g_congruence.ml
+plugins/ring/g_ring.ml
+plugins/field/field.ml
+plugins/funind/g_indfun.ml
+plugins/omega/g_omega.ml
+plugins/quote/g_quote.ml
+plugins/nsatz/nsatz.ml
+plugins/micromega/g_micromega.ml
+plugins/subtac/g_subtac.ml
+plugins/fourier/g_fourier.ml
+plugins/decl_mode/g_decl_mode.ml
+tactics/tauto.ml
+tactics/eauto.ml
+tactics/hipattern.ml
+tactics/class_tactics.ml
+tactics/rewrite.ml
+tactics/eqdecide.ml
+tactics/extratactics.ml
+tactics/extraargs.ml
+tools/coq_tex.ml
+toplevel/mltop.ml
+toplevel/whelp.ml
+ide/coqide_main.ml
+ide/coqide_main_opt.ml
+
+# other auto-generated files
+
+ide/undo.mli
+toplevel/mltop.optml
+toplevel/mltop.byteml
+kernel/byterun/coq_jumptbl.h
+kernel/copcodes.ml
+scripts/tolink.ml
+theories/Numbers/Natural/BigN/NMake_gen.v
+ide/index_urls.txt
+
+# mlis documentation
+
+dev/ocamldoc/html/
+dev/ocamldoc/coq.*
+dev/ocamldoc/ocamldoc.sty