Fix the build of coq via ocamlbuild

 - no more plugins/interface
 - a few missing files in theories.itarget
 - a few things required Unix now

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

7 files changed, 14 insertions, 16 deletions

diff --git a/_tags b/_tags
index 97957e81e..6f83b4ef3 100644
--- a/_tags
+++ b/_tags
@@ -9,12 +9,16 @@
 <tools/coq_makefile.{native,byte}> : use_str
 <tools/coqdoc/main.{native,byte}> : use_str
 <checker/main.{native,byte}> : use_str, use_unix, use_gramlib
-<plugins/micromega/csdpcert.{native,byte}> : use_nums
+<plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix
 
 ## tags for ide
 
 <ide/**/*.{ml,mli}>: thread, ide
 
+## tags for grammar.cm*
+
+<parsing/grammar.{cma,cmxa}> : use_unix
+
 ## tags for camlp4 files 
 
 <**/*.ml4>: is_ml4
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 963adcc7c..f7c014aba 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -124,18 +124,18 @@ let theoriesv =
   let vo = string_list_of_file "theories/theories.itarget" in
   List.map (fun s -> "theories/"^(Filename.chop_suffix s "o")) vo
 
-let contribv =
+let pluginsv =
   let vo = string_list_of_file "plugins/pluginsvo.itarget" in
   List.map (fun s -> "plugins/"^(Filename.chop_suffix s "o")) vo
 
-let contribmllib =
+let pluginsmllib =
   let cma = string_list_of_file "plugins/pluginsbyte.itarget" in
   List.map (fun s -> "plugins/"^(Filename.chop_suffix s ".cma")^".mllib") cma
 
 (** for correct execution of coqdep_boot, source files should have
     been imported in _build (and NMake.v should have been created). *)
 
-let coqdepdeps = theoriesv @ contribv @ contribmllib
+let coqdepdeps = theoriesv @ pluginsv @ pluginsmllib
 
 let coqtop = "toplevel/coqtop"
 let coqide = "ide/coqide"
@@ -209,9 +209,11 @@ let incl f = Ocaml_utils.ocaml_include_flags f
 let cmd cl = (fun _ _ -> (Cmd (S cl)))
 
 let initial_actions () = begin
-  make_bin_links all_binaries;
-  (** We "pre-create" a few subdirs in _build to please coqtop *)
+  (** We "pre-create" a few subdirs in _build *)
   Shell.mkdir_p (!_build^"/dev");
+  Shell.mkdir_p (!_build^"/bin");
+  Shell.mkdir_p (!_build^"/plugins/micromega");
+  make_bin_links all_binaries;
 end
 
 let extra_rules () = begin
diff --git a/plugins/_tags b/plugins/_tags
index 6d28450fd..f95e0c5b8 100644
--- a/plugins/_tags
+++ b/plugins/_tags
@@ -3,8 +3,6 @@
 "cc/g_congruence.ml4": use_grammar
 "setoid_ring/newring.ml4": use_grammar
 "dp/g_dp.ml4": use_grammar
-"interface/centaur.ml4": use_grammar
-"interface/debug_tac.ml4": use_grammar
 "quote/g_quote.ml4": use_grammar
 "subtac/equations.ml4": use_grammar, use_extend
 "subtac/g_eterm.ml4": use_grammar
@@ -23,12 +21,10 @@
 "groebner/ideal.ml4": use_refutpat
 "groebner/groebner.ml4": use_grammar
 
-
 "cc": include
 "extraction": include
 "firstorder": include
 "funind": include
-"interface": include
 "micromega": include
 "quote": include
 "romega": include
diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget
index 7e0a77787..7ca8020dc 100644
--- a/plugins/pluginsbyte.itarget
+++ b/plugins/pluginsbyte.itarget
@@ -3,8 +3,6 @@ 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
diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget
index e8e7868b7..520627115 100644
--- a/plugins/pluginsopt.itarget
+++ b/plugins/pluginsopt.itarget
@@ -3,8 +3,6 @@ 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
diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget
index af4d23310..14c288005 100644
--- a/plugins/pluginsvo.itarget
+++ b/plugins/pluginsvo.itarget
@@ -8,8 +8,6 @@ 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
diff --git a/theories/theories.itarget b/theories/theories.itarget
index 019047ef5..99b059f51 100644
--- a/theories/theories.itarget
+++ b/theories/theories.itarget
@@ -42,6 +42,7 @@ Classes/SetoidAxioms.vo
 Classes/SetoidClass.vo
 Classes/SetoidDec.vo
 Classes/SetoidTactics.vo
+Classes/RelationPairs.vo
 
 FSets/FMapAVL.vo
 FSets/FMapFacts.vo
@@ -89,6 +90,7 @@ Structures/DecidableType2.vo
 Structures/DecidableType2Ex.vo
 Structures/DecidableType2Facts.vo
 Structures/OrderTac.vo
+Structures/GenericMinMax.vo
 
 Init/Datatypes.vo
 Init/Logic_Type.vo