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

4 files changed, 0 insertions, 10 deletions

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