Ocamlbuild: improvements suggested by N. Pouillard

 * Import of Coq_config via myocamlbuild_config.ml, instead of my get_env
 * As a consequence, we enrich this Coq_config with stuff that was
   only in config/Makefile
 * replace the big ugly find by some dependencies against source files
 * by the way: build csdpcert, with the right aliases.

I've tried to escape things properly for windows in ./configure,
but this isn't fully tested yet.

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

4 files changed, 113 insertions, 0 deletions

diff --git a/plugins/plugins.itarget b/plugins/plugins.itarget
new file mode 100644
index 0000000000..56aa42b069
--- /dev/null
+++ b/plugins/plugins.itarget
@@ -0,0 +1,3 @@
+pluginsopt.otarget
+pluginsbyte.otarget
+pluginsvo.otarget
\ No newline at end of file
diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget
new file mode 100644
index 0000000000..7e0a777874
--- /dev/null
+++ b/plugins/pluginsbyte.itarget
@@ -0,0 +1,25 @@
+field/field_plugin.cma
+setoid_ring/newring_plugin.cma
+extraction/extraction_plugin.cma
+firstorder/ground_plugin.cma
+rtauto/rtauto_plugin.cma
+interface/coqinterface_plugin.cma
+interface/coqparser_plugin.cma
+fourier/fourier_plugin.cma
+romega/romega_plugin.cma
+omega/omega_plugin.cma
+micromega/micromega_plugin.cma
+dp/dp_plugin.cma
+xml/xml_plugin.cma
+subtac/subtac_plugin.cma
+ring/ring_plugin.cma
+cc/cc_plugin.cma
+groebner/groebner_plugin.cma
+funind/recdef_plugin.cma
+syntax/ascii_syntax_plugin.cma
+syntax/nat_syntax_plugin.cma
+syntax/numbers_syntax_plugin.cma
+syntax/r_syntax_plugin.cma
+syntax/string_syntax_plugin.cma
+syntax/z_syntax_plugin.cma
+quote/quote_plugin.cma
diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget
new file mode 100644
index 0000000000..e8e7868b76
--- /dev/null
+++ b/plugins/pluginsopt.itarget
@@ -0,0 +1,25 @@
+field/field_plugin.cmxa
+setoid_ring/newring_plugin.cmxa
+extraction/extraction_plugin.cmxa
+firstorder/ground_plugin.cmxa
+rtauto/rtauto_plugin.cmxa
+interface/coqinterface_plugin.cmxa
+interface/coqparser_plugin.cmxa
+fourier/fourier_plugin.cmxa
+romega/romega_plugin.cmxa
+omega/omega_plugin.cmxa
+micromega/micromega_plugin.cmxa
+dp/dp_plugin.cmxa
+xml/xml_plugin.cmxa
+subtac/subtac_plugin.cmxa
+ring/ring_plugin.cmxa
+cc/cc_plugin.cmxa
+groebner/groebner_plugin.cmxa
+funind/recdef_plugin.cmxa
+syntax/ascii_syntax_plugin.cmxa
+syntax/nat_syntax_plugin.cmxa
+syntax/numbers_syntax_plugin.cmxa
+syntax/r_syntax_plugin.cmxa
+syntax/string_syntax_plugin.cmxa
+syntax/z_syntax_plugin.cmxa
+quote/quote_plugin.cmxa
diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget
new file mode 100644
index 0000000000..af4d233102
--- /dev/null
+++ b/plugins/pluginsvo.itarget
@@ -0,0 +1,60 @@
+dp/Dp.vo
+field/LegacyField_Compl.vo
+field/LegacyField_Tactic.vo
+field/LegacyField_Theory.vo
+field/LegacyField.vo
+fourier/Fourier_util.vo
+fourier/Fourier.vo
+funind/Recdef.vo
+groebner/GroebnerR.vo
+groebner/GroebnerZ.vo
+interface/CoqInterface.vo
+#interface/CoqParser.vo  (should not be compiled)
+micromega/CheckerMaker.vo
+micromega/EnvRing.vo
+micromega/Env.vo
+#micromega/MExtraction.vo  (extraction of micromega.ml)
+micromega/OrderedRing.vo
+micromega/Psatz.vo
+micromega/QMicromega.vo
+micromega/Refl.vo
+micromega/RingMicromega.vo
+micromega/RMicromega.vo
+micromega/Tauto.vo
+micromega/VarMap.vo
+micromega/ZCoeff.vo
+micromega/ZMicromega.vo
+omega/OmegaLemmas.vo
+omega/OmegaPlugin.vo
+omega/Omega.vo
+omega/PreOmega.vo
+quote/Quote.vo
+ring/LegacyArithRing.vo
+ring/LegacyNArithRing.vo
+ring/LegacyRing_theory.vo
+ring/LegacyRing.vo
+ring/LegacyZArithRing.vo
+ring/Ring_abstract.vo
+ring/Ring_normalize.vo
+ring/Setoid_ring_normalize.vo
+ring/Setoid_ring_theory.vo
+ring/Setoid_ring.vo
+romega/ReflOmegaCore.vo
+romega/ROmega.vo
+rtauto/Bintree.vo
+rtauto/Rtauto.vo
+setoid_ring/ArithRing.vo
+setoid_ring/BinList.vo
+setoid_ring/Field_tac.vo
+setoid_ring/Field_theory.vo
+setoid_ring/Field.vo
+setoid_ring/InitialRing.vo
+setoid_ring/NArithRing.vo
+setoid_ring/RealField.vo
+setoid_ring/Ring_base.vo
+setoid_ring/Ring_equiv.vo
+setoid_ring/Ring_polynom.vo
+setoid_ring/Ring_tac.vo
+setoid_ring/Ring_theory.vo
+setoid_ring/Ring.vo
+setoid_ring/ZArithRing.vo