From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 .gitignore | 138 +++++++++++++++++++++++++++++++++++++++++++++++--------------
 1 file changed, 106 insertions(+), 32 deletions(-)

(limited to '.gitignore')

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
-- 
cgit v1.2.3