diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-03 14:51:52 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-03 14:51:52 +0000 |
commit | 141a21da29216a43eb067ef0fcb9c7d914d45bdc (patch) | |
tree | 0450a0d679dd04412427b452cd8acfcaa8225d64 /plugins/pluginsvo.itarget | |
parent | b2d7dfd0ab28846748fe2f903ee567e7705623da (diff) |
Ocamlbuild: improvements suggested by N. Pouillard
* Import of Coq_config via myocamlbuild_config.ml, instead of my get_env
* As a consequence, we enrich this Coq_config with stuff that was
only in config/Makefile
* replace the big ugly find by some dependencies against source files
* by the way: build csdpcert, with the right aliases.
I've tried to escape things properly for windows in ./configure,
but this isn't fully tested yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12046 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/pluginsvo.itarget')
-rw-r--r-- | plugins/pluginsvo.itarget | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget new file mode 100644 index 000000000..af4d23310 --- /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 |