From eb93dfaceccbba06f62eb92ef5e12a133c7959d4 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 14 Mar 2009 11:29:46 +0000 Subject: 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 --- contrib/cc/cc_plugin.mllib | 4 ++++ contrib/dp/dp_plugin.mllib | 5 +++++ contrib/extraction/extraction_plugin.mllib | 10 ++++++++++ contrib/field/field_plugin.mllib | 1 + contrib/firstorder/ground_plugin.mllib | 7 +++++++ contrib/fourier/fourier_plugin.mllib | 3 +++ contrib/funind/recdef_plugin.mllib | 10 ++++++++++ contrib/groebner/groebner_plugin.mllib | 4 ++++ contrib/interface/coqinterface_plugin.mllib | 14 ++++++++++++++ contrib/interface/coqparser_plugin.mllib | 4 ++++ contrib/micromega/micromega_plugin.mllib | 6 ++++++ contrib/omega/omega_plugin.mllib | 3 +++ contrib/quote/quote_plugin.mllib | 2 ++ contrib/ring/ring_plugin.mllib | 2 ++ contrib/romega/romega_plugin.mllib | 3 +++ contrib/rtauto/rtauto_plugin.mllib | 3 +++ contrib/setoid_ring/newring_plugin.mllib | 1 + contrib/subtac/subtac_plugin.mllib | 14 ++++++++++++++ contrib/xml/xml_plugin.mllib | 12 ++++++++++++ 19 files changed, 108 insertions(+) create mode 100644 contrib/cc/cc_plugin.mllib create mode 100644 contrib/dp/dp_plugin.mllib create mode 100644 contrib/extraction/extraction_plugin.mllib create mode 100644 contrib/field/field_plugin.mllib create mode 100644 contrib/firstorder/ground_plugin.mllib create mode 100644 contrib/fourier/fourier_plugin.mllib create mode 100644 contrib/funind/recdef_plugin.mllib create mode 100644 contrib/groebner/groebner_plugin.mllib create mode 100644 contrib/interface/coqinterface_plugin.mllib create mode 100644 contrib/interface/coqparser_plugin.mllib create mode 100644 contrib/micromega/micromega_plugin.mllib create mode 100644 contrib/omega/omega_plugin.mllib create mode 100644 contrib/quote/quote_plugin.mllib create mode 100644 contrib/ring/ring_plugin.mllib create mode 100644 contrib/romega/romega_plugin.mllib create mode 100644 contrib/rtauto/rtauto_plugin.mllib create mode 100644 contrib/setoid_ring/newring_plugin.mllib create mode 100644 contrib/subtac/subtac_plugin.mllib create mode 100644 contrib/xml/xml_plugin.mllib (limited to 'contrib') 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 -- cgit v1.2.3