diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/plugins.itarget | 3 | ||||
| -rw-r--r-- | plugins/pluginsbyte.itarget | 25 | ||||
| -rw-r--r-- | plugins/pluginsopt.itarget | 25 | ||||
| -rw-r--r-- | plugins/pluginsvo.itarget | 60 |
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 |
