Makefile: ml dependencies of contribs are moved to .mllib files

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

19 files changed, 108 insertions, 0 deletions

diff --git a/contrib/cc/cc_plugin.mllib b/contrib/cc/cc_plugin.mllib
new file mode 100644
index 0000000000..27e903fd38
--- /dev/null
+++ b/contrib/cc/cc_plugin.mllib
@@ -0,0 +1,4 @@
+Ccalgo
+Ccproof
+Cctac
+G_congruence
diff --git a/contrib/dp/dp_plugin.mllib b/contrib/dp/dp_plugin.mllib
new file mode 100644
index 0000000000..361d6f8323
--- /dev/null
+++ b/contrib/dp/dp_plugin.mllib
@@ -0,0 +1,5 @@
+Dp_why
+Dp_zenon
+Dp
+Dp_gappa
+G_dp
diff --git a/contrib/extraction/extraction_plugin.mllib b/contrib/extraction/extraction_plugin.mllib
new file mode 100644
index 0000000000..bb87b9e325
--- /dev/null
+++ b/contrib/extraction/extraction_plugin.mllib
@@ -0,0 +1,10 @@
+Table
+Mlutil
+Modutil
+Extraction
+Common
+Ocaml
+Haskell
+Scheme
+Extract_env
+G_extraction
diff --git a/contrib/field/field_plugin.mllib b/contrib/field/field_plugin.mllib
new file mode 100644
index 0000000000..63492a64f0
--- /dev/null
+++ b/contrib/field/field_plugin.mllib
@@ -0,0 +1 @@
+Field
diff --git a/contrib/firstorder/ground_plugin.mllib b/contrib/firstorder/ground_plugin.mllib
new file mode 100644
index 0000000000..863ccb50e8
--- /dev/null
+++ b/contrib/firstorder/ground_plugin.mllib
@@ -0,0 +1,7 @@
+Formula
+Unify
+Sequent
+Rules
+Instances
+Ground 
+G_ground
\ No newline at end of file
diff --git a/contrib/fourier/fourier_plugin.mllib b/contrib/fourier/fourier_plugin.mllib
new file mode 100644
index 0000000000..b6262f8aeb
--- /dev/null
+++ b/contrib/fourier/fourier_plugin.mllib
@@ -0,0 +1,3 @@
+Fourier
+FourierR
+G_fourier
diff --git a/contrib/funind/recdef_plugin.mllib b/contrib/funind/recdef_plugin.mllib
new file mode 100644
index 0000000000..c30ee212f5
--- /dev/null
+++ b/contrib/funind/recdef_plugin.mllib
@@ -0,0 +1,10 @@
+Indfun_common
+Rawtermops
+Recdef
+Rawterm_to_relation
+Functional_principles_proofs
+Functional_principles_types
+Invfun
+Indfun
+Merge
+G_indfun
diff --git a/contrib/groebner/groebner_plugin.mllib b/contrib/groebner/groebner_plugin.mllib
new file mode 100644
index 0000000000..1da12fcf2e
--- /dev/null
+++ b/contrib/groebner/groebner_plugin.mllib
@@ -0,0 +1,4 @@
+Utile
+Polynom
+Ideal
+Groebner
diff --git a/contrib/interface/coqinterface_plugin.mllib b/contrib/interface/coqinterface_plugin.mllib
new file mode 100644
index 0000000000..e4b575b136
--- /dev/null
+++ b/contrib/interface/coqinterface_plugin.mllib
@@ -0,0 +1,14 @@
+Vtp
+Xlate
+Paths
+Translate
+Pbp
+Dad
+History
+Name_to_ast
+Debug_tac
+Showproof_ct
+Showproof
+Blast
+Depends
+Centaur
diff --git a/contrib/interface/coqparser_plugin.mllib b/contrib/interface/coqparser_plugin.mllib
new file mode 100644
index 0000000000..65ec577153
--- /dev/null
+++ b/contrib/interface/coqparser_plugin.mllib
@@ -0,0 +1,4 @@
+Line_parser
+Vtp
+Xlate
+Coqparser
\ No newline at end of file
diff --git a/contrib/micromega/micromega_plugin.mllib b/contrib/micromega/micromega_plugin.mllib
new file mode 100644
index 0000000000..41753542f6
--- /dev/null
+++ b/contrib/micromega/micromega_plugin.mllib
@@ -0,0 +1,6 @@
+Mutils
+Micromega
+Mfourier
+Certificate
+Coq_micromega
+G_micromega
diff --git a/contrib/omega/omega_plugin.mllib b/contrib/omega/omega_plugin.mllib
new file mode 100644
index 0000000000..0209013762
--- /dev/null
+++ b/contrib/omega/omega_plugin.mllib
@@ -0,0 +1,3 @@
+Omega
+Coq_omega
+G_omega
\ No newline at end of file
diff --git a/contrib/quote/quote_plugin.mllib b/contrib/quote/quote_plugin.mllib
new file mode 100644
index 0000000000..21810acdff
--- /dev/null
+++ b/contrib/quote/quote_plugin.mllib
@@ -0,0 +1,2 @@
+Quote
+G_quote
\ No newline at end of file
diff --git a/contrib/ring/ring_plugin.mllib b/contrib/ring/ring_plugin.mllib
new file mode 100644
index 0000000000..183884ca6d
--- /dev/null
+++ b/contrib/ring/ring_plugin.mllib
@@ -0,0 +1,2 @@
+Ring
+G_ring
diff --git a/contrib/romega/romega_plugin.mllib b/contrib/romega/romega_plugin.mllib
new file mode 100644
index 0000000000..38d0e94111
--- /dev/null
+++ b/contrib/romega/romega_plugin.mllib
@@ -0,0 +1,3 @@
+Const_omega
+Refl_omega
+G_romega
diff --git a/contrib/rtauto/rtauto_plugin.mllib b/contrib/rtauto/rtauto_plugin.mllib
new file mode 100644
index 0000000000..61c5e945bc
--- /dev/null
+++ b/contrib/rtauto/rtauto_plugin.mllib
@@ -0,0 +1,3 @@
+Proof_search
+Refl_tauto
+G_rtauto
diff --git a/contrib/setoid_ring/newring_plugin.mllib b/contrib/setoid_ring/newring_plugin.mllib
new file mode 100644
index 0000000000..54b7c8e676
--- /dev/null
+++ b/contrib/setoid_ring/newring_plugin.mllib
@@ -0,0 +1 @@
+Newring
diff --git a/contrib/subtac/subtac_plugin.mllib b/contrib/subtac/subtac_plugin.mllib
new file mode 100644
index 0000000000..81b9ee2bab
--- /dev/null
+++ b/contrib/subtac/subtac_plugin.mllib
@@ -0,0 +1,14 @@
+Subtac_utils
+Eterm
+G_eterm
+Subtac_errors
+Subtac_coercion
+Subtac_obligations
+Subtac_cases
+Subtac_pretyping_F
+Subtac_pretyping
+Subtac_command
+Subtac_classes
+Subtac
+G_subtac
+Equations
diff --git a/contrib/xml/xml_plugin.mllib b/contrib/xml/xml_plugin.mllib
new file mode 100644
index 0000000000..3297ff0684
--- /dev/null
+++ b/contrib/xml/xml_plugin.mllib
@@ -0,0 +1,12 @@
+Unshare
+Xml
+Acic
+DoubleTypeInference
+Cic2acic
+Acic2Xml
+Proof2aproof
+Xmlcommand
+ProofTree2Xml
+Xmlentries
+Cic2Xml
+Dumptree