diff options
author | 2012-01-12 16:08:29 +0100 | |
---|---|---|
committer | 2012-01-12 16:08:29 +0100 | |
commit | 23a6061a81ffa0c214d521287b6af0a31bfa22f0 (patch) | |
tree | f1ca9ba9240b98b8695a9f1870e56602734cf97c /.gitignore | |
parent | de109d8c0c68f569b907e6e24271f259ba28888e (diff) | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) |
Merge commit 'upstream/8.4_beta+dfsg' into experimental/master
Diffstat (limited to '.gitignore')
-rw-r--r-- | .gitignore | 138 |
1 files changed, 106 insertions, 32 deletions
@@ -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 |