Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)

- This way, the Makefile.build gets shorter and simplier, with a few nasty
   hacks removed.
 - In particular, we stop creating dummy .ml of .ml4 early "to please ocamldep".
   Instead, we now use ocamldep -modules, and process its output via coqdep_boot.
   This ways, *.cm* of .ml4 are correctly located, even when some .ml files
   aren't generated yet.
 - There is no risk of editing the .ml of a .ml4 by mistake, since it is by
   default in a binary format (cf pr_o.cmo and variable READABLE_ML4).
   M-x next-error still open the right .ml4 at the right location.
 - mltop.byteml is now mltop.ml, while mltop.optml keeps its name
 - .ml of .ml4 are added to .gitignore

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12833 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 96 insertions, 30 deletions

diff --git a/.gitignore b/.gitignore
index 8b735ec5a..e96978b4c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -37,39 +37,21 @@
 *.v.html
 revision
 TAGS
+.DS_Store
 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
-theories/Numbers/Natural/BigN/NMake_gen.v
-tools/coqdep_lexer.ml
-tools/coqdoc/index.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
+
+# documentation
+
 doc/faq/html/
 doc/refman/Reference-Manual.pdf
 doc/refman/Reference-Manual.ps
@@ -96,7 +78,91 @@ 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
+
+# .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/index.ml
+tools/coqdoc/cpretty.ml
+
+# .mly files
+
+dev/ocamlweb-doc/syntax.ml
+dev/ocamlweb-doc/syntax.mli
+ide/config_parser.ml
+ide/config_parser.mli
+
+# .ml4 files
+
+lib/pp.ml
+lib/compat.ml
+lib/refutpat.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/groebner/groebner.ml
+plugins/groebner/ideal.ml
+plugins/micromega/g_micromega.ml
+plugins/subtac/g_subtac.ml
+plugins/fourier/g_fourier.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_makefile.ml
+tools/coq_tex.ml
+toplevel/mltop.ml
+toplevel/whelp.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