aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-03-20 01:22:58 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-03-20 01:22:58 +0000
commit7d220f8b61649646692983872626d6a8042446a9 (patch)
treefefceb2c59cf155c55fffa25ad08bec629de523e
parentad1fea78e3c23c903b2256d614756012d5f05d87 (diff)
Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--CHANGES10
-rw-r--r--COPYRIGHT10
-rw-r--r--CREDITS36
-rw-r--r--Makefile4
-rw-r--r--Makefile.build28
-rw-r--r--Makefile.common106
-rw-r--r--Makefile.doc2
-rw-r--r--checker/checker.ml6
-rw-r--r--config/coq_config.mli2
-rwxr-xr-xconfigure4
-rw-r--r--dev/doc/changes.txt2
-rw-r--r--dev/ocamldebug-coq.template16
-rw-r--r--dev/ocamlweb-doc/Makefile16
-rw-r--r--dev/v8-syntax/syntax-v8.tex18
-rw-r--r--doc/faq/FAQ.tex2
-rw-r--r--doc/refman/Extraction.tex4
-rw-r--r--doc/refman/Helm.tex2
-rw-r--r--doc/refman/Polynom.tex12
-rw-r--r--doc/refman/RefMan-tac.tex2
-rw-r--r--doc/refman/RefMan-tacex.tex2
-rw-r--r--doc/refman/RefMan-tus.tex3
-rw-r--r--plugins/cc/README (renamed from contrib/cc/README)0
-rw-r--r--plugins/cc/cc_plugin.mllib (renamed from contrib/cc/cc_plugin.mllib)0
-rw-r--r--plugins/cc/ccalgo.ml (renamed from contrib/cc/ccalgo.ml)0
-rw-r--r--plugins/cc/ccalgo.mli (renamed from contrib/cc/ccalgo.mli)0
-rw-r--r--plugins/cc/ccproof.ml (renamed from contrib/cc/ccproof.ml)0
-rw-r--r--plugins/cc/ccproof.mli (renamed from contrib/cc/ccproof.mli)0
-rw-r--r--plugins/cc/cctac.ml (renamed from contrib/cc/cctac.ml)0
-rw-r--r--plugins/cc/cctac.mli (renamed from contrib/cc/cctac.mli)0
-rw-r--r--plugins/cc/g_congruence.ml4 (renamed from contrib/cc/g_congruence.ml4)0
-rw-r--r--plugins/dp/Dp.v (renamed from contrib/dp/Dp.v)0
-rw-r--r--plugins/dp/TODO (renamed from contrib/dp/TODO)0
-rw-r--r--plugins/dp/dp.ml (renamed from contrib/dp/dp.ml)0
-rw-r--r--plugins/dp/dp.mli (renamed from contrib/dp/dp.mli)0
-rw-r--r--plugins/dp/dp_gappa.ml (renamed from contrib/dp/dp_gappa.ml)0
-rw-r--r--plugins/dp/dp_plugin.mllib (renamed from contrib/dp/dp_plugin.mllib)0
-rw-r--r--plugins/dp/dp_why.ml (renamed from contrib/dp/dp_why.ml)0
-rw-r--r--plugins/dp/dp_why.mli (renamed from contrib/dp/dp_why.mli)0
-rw-r--r--plugins/dp/dp_zenon.mli (renamed from contrib/dp/dp_zenon.mli)0
-rw-r--r--plugins/dp/dp_zenon.mll (renamed from contrib/dp/dp_zenon.mll)0
-rw-r--r--plugins/dp/fol.mli (renamed from contrib/dp/fol.mli)0
-rw-r--r--plugins/dp/g_dp.ml4 (renamed from contrib/dp/g_dp.ml4)0
-rw-r--r--plugins/dp/test2.v (renamed from contrib/dp/test2.v)0
-rw-r--r--plugins/dp/test_gappa.v (renamed from contrib/dp/test_gappa.v)0
-rw-r--r--plugins/dp/tests.v (renamed from contrib/dp/tests.v)2
-rw-r--r--plugins/dp/zenon.v (renamed from contrib/dp/zenon.v)0
-rw-r--r--plugins/extraction/CHANGES (renamed from contrib/extraction/CHANGES)2
-rw-r--r--plugins/extraction/README (renamed from contrib/extraction/README)0
-rw-r--r--plugins/extraction/common.ml (renamed from contrib/extraction/common.ml)0
-rw-r--r--plugins/extraction/common.mli (renamed from contrib/extraction/common.mli)0
-rw-r--r--plugins/extraction/extract_env.ml (renamed from contrib/extraction/extract_env.ml)0
-rw-r--r--plugins/extraction/extract_env.mli (renamed from contrib/extraction/extract_env.mli)0
-rw-r--r--plugins/extraction/extraction.ml (renamed from contrib/extraction/extraction.ml)0
-rw-r--r--plugins/extraction/extraction.mli (renamed from contrib/extraction/extraction.mli)0
-rw-r--r--plugins/extraction/extraction_plugin.mllib (renamed from contrib/extraction/extraction_plugin.mllib)0
-rw-r--r--plugins/extraction/g_extraction.ml4 (renamed from contrib/extraction/g_extraction.ml4)0
-rw-r--r--plugins/extraction/haskell.ml (renamed from contrib/extraction/haskell.ml)0
-rw-r--r--plugins/extraction/haskell.mli (renamed from contrib/extraction/haskell.mli)0
-rw-r--r--plugins/extraction/miniml.mli (renamed from contrib/extraction/miniml.mli)0
-rw-r--r--plugins/extraction/mlutil.ml (renamed from contrib/extraction/mlutil.ml)0
-rw-r--r--plugins/extraction/mlutil.mli (renamed from contrib/extraction/mlutil.mli)0
-rw-r--r--plugins/extraction/modutil.ml (renamed from contrib/extraction/modutil.ml)0
-rw-r--r--plugins/extraction/modutil.mli (renamed from contrib/extraction/modutil.mli)0
-rw-r--r--plugins/extraction/ocaml.ml (renamed from contrib/extraction/ocaml.ml)0
-rw-r--r--plugins/extraction/ocaml.mli (renamed from contrib/extraction/ocaml.mli)0
-rw-r--r--plugins/extraction/scheme.ml (renamed from contrib/extraction/scheme.ml)0
-rw-r--r--plugins/extraction/scheme.mli (renamed from contrib/extraction/scheme.mli)0
-rw-r--r--plugins/extraction/table.ml (renamed from contrib/extraction/table.ml)0
-rw-r--r--plugins/extraction/table.mli (renamed from contrib/extraction/table.mli)0
-rw-r--r--plugins/field/LegacyField.v (renamed from contrib/field/LegacyField.v)0
-rw-r--r--plugins/field/LegacyField_Compl.v (renamed from contrib/field/LegacyField_Compl.v)0
-rw-r--r--plugins/field/LegacyField_Tactic.v (renamed from contrib/field/LegacyField_Tactic.v)0
-rw-r--r--plugins/field/LegacyField_Theory.v (renamed from contrib/field/LegacyField_Theory.v)0
-rw-r--r--plugins/field/field.ml4 (renamed from contrib/field/field.ml4)0
-rw-r--r--plugins/field/field_plugin.mllib (renamed from contrib/field/field_plugin.mllib)0
-rw-r--r--plugins/firstorder/formula.ml (renamed from contrib/firstorder/formula.ml)0
-rw-r--r--plugins/firstorder/formula.mli (renamed from contrib/firstorder/formula.mli)0
-rw-r--r--plugins/firstorder/g_ground.ml4 (renamed from contrib/firstorder/g_ground.ml4)0
-rw-r--r--plugins/firstorder/ground.ml (renamed from contrib/firstorder/ground.ml)0
-rw-r--r--plugins/firstorder/ground.mli (renamed from contrib/firstorder/ground.mli)0
-rw-r--r--plugins/firstorder/ground_plugin.mllib (renamed from contrib/firstorder/ground_plugin.mllib)0
-rw-r--r--plugins/firstorder/instances.ml (renamed from contrib/firstorder/instances.ml)0
-rw-r--r--plugins/firstorder/instances.mli (renamed from contrib/firstorder/instances.mli)0
-rw-r--r--plugins/firstorder/rules.ml (renamed from contrib/firstorder/rules.ml)0
-rw-r--r--plugins/firstorder/rules.mli (renamed from contrib/firstorder/rules.mli)0
-rw-r--r--plugins/firstorder/sequent.ml (renamed from contrib/firstorder/sequent.ml)0
-rw-r--r--plugins/firstorder/sequent.mli (renamed from contrib/firstorder/sequent.mli)0
-rw-r--r--plugins/firstorder/unify.ml (renamed from contrib/firstorder/unify.ml)0
-rw-r--r--plugins/firstorder/unify.mli (renamed from contrib/firstorder/unify.mli)0
-rw-r--r--plugins/fourier/Fourier.v (renamed from contrib/fourier/Fourier.v)0
-rw-r--r--plugins/fourier/Fourier_util.v (renamed from contrib/fourier/Fourier_util.v)0
-rw-r--r--plugins/fourier/fourier.ml (renamed from contrib/fourier/fourier.ml)0
-rw-r--r--plugins/fourier/fourierR.ml (renamed from contrib/fourier/fourierR.ml)0
-rw-r--r--plugins/fourier/fourier_plugin.mllib (renamed from contrib/fourier/fourier_plugin.mllib)0
-rw-r--r--plugins/fourier/g_fourier.ml4 (renamed from contrib/fourier/g_fourier.ml4)0
-rw-r--r--plugins/funind/Recdef.v (renamed from contrib/funind/Recdef.v)0
-rw-r--r--plugins/funind/functional_principles_proofs.ml (renamed from contrib/funind/functional_principles_proofs.ml)0
-rw-r--r--plugins/funind/functional_principles_proofs.mli (renamed from contrib/funind/functional_principles_proofs.mli)0
-rw-r--r--plugins/funind/functional_principles_types.ml (renamed from contrib/funind/functional_principles_types.ml)0
-rw-r--r--plugins/funind/functional_principles_types.mli (renamed from contrib/funind/functional_principles_types.mli)0
-rw-r--r--plugins/funind/g_indfun.ml4 (renamed from contrib/funind/g_indfun.ml4)0
-rw-r--r--plugins/funind/indfun.ml (renamed from contrib/funind/indfun.ml)0
-rw-r--r--plugins/funind/indfun_common.ml (renamed from contrib/funind/indfun_common.ml)0
-rw-r--r--plugins/funind/indfun_common.mli (renamed from contrib/funind/indfun_common.mli)0
-rw-r--r--plugins/funind/invfun.ml (renamed from contrib/funind/invfun.ml)0
-rw-r--r--plugins/funind/merge.ml (renamed from contrib/funind/merge.ml)2
-rw-r--r--plugins/funind/rawterm_to_relation.ml (renamed from contrib/funind/rawterm_to_relation.ml)0
-rw-r--r--plugins/funind/rawterm_to_relation.mli (renamed from contrib/funind/rawterm_to_relation.mli)0
-rw-r--r--plugins/funind/rawtermops.ml (renamed from contrib/funind/rawtermops.ml)0
-rw-r--r--plugins/funind/rawtermops.mli (renamed from contrib/funind/rawtermops.mli)0
-rw-r--r--plugins/funind/recdef.ml (renamed from contrib/funind/recdef.ml)0
-rw-r--r--plugins/funind/recdef_plugin.mllib (renamed from contrib/funind/recdef_plugin.mllib)0
-rw-r--r--plugins/groebner/GroebnerR.v (renamed from contrib/groebner/GroebnerR.v)0
-rw-r--r--plugins/groebner/GroebnerZ.v (renamed from contrib/groebner/GroebnerZ.v)0
-rw-r--r--plugins/groebner/groebner.ml4 (renamed from contrib/groebner/groebner.ml4)0
-rw-r--r--plugins/groebner/groebner_plugin.mllib (renamed from contrib/groebner/groebner_plugin.mllib)0
-rw-r--r--plugins/groebner/ideal.ml (renamed from contrib/groebner/ideal.ml)0
-rw-r--r--plugins/groebner/ideal.mli (renamed from contrib/groebner/ideal.mli)0
-rw-r--r--plugins/groebner/polynom.ml (renamed from contrib/groebner/polynom.ml)0
-rw-r--r--plugins/groebner/polynom.mli (renamed from contrib/groebner/polynom.mli)0
-rw-r--r--plugins/groebner/utile.ml (renamed from contrib/groebner/utile.ml)0
-rw-r--r--plugins/groebner/utile.mli (renamed from contrib/groebner/utile.mli)0
-rw-r--r--plugins/interface/COPYRIGHT (renamed from contrib/interface/COPYRIGHT)2
-rw-r--r--plugins/interface/CoqInterface.v (renamed from contrib/interface/CoqInterface.v)0
-rw-r--r--plugins/interface/CoqParser.v (renamed from contrib/interface/CoqParser.v)0
-rw-r--r--plugins/interface/ascent.mli (renamed from contrib/interface/ascent.mli)0
-rw-r--r--plugins/interface/blast.ml (renamed from contrib/interface/blast.ml)0
-rw-r--r--plugins/interface/blast.mli (renamed from contrib/interface/blast.mli)0
-rw-r--r--plugins/interface/centaur.ml4 (renamed from contrib/interface/centaur.ml4)0
-rw-r--r--plugins/interface/coqinterface_plugin.mllib (renamed from contrib/interface/coqinterface_plugin.mllib)0
-rw-r--r--plugins/interface/coqparser.ml (renamed from contrib/interface/coqparser.ml)4
-rw-r--r--plugins/interface/coqparser_plugin.mllib (renamed from contrib/interface/coqparser_plugin.mllib)0
-rw-r--r--plugins/interface/dad.ml (renamed from contrib/interface/dad.ml)0
-rw-r--r--plugins/interface/dad.mli (renamed from contrib/interface/dad.mli)0
-rw-r--r--plugins/interface/debug_tac.ml4 (renamed from contrib/interface/debug_tac.ml4)0
-rw-r--r--plugins/interface/debug_tac.mli (renamed from contrib/interface/debug_tac.mli)0
-rw-r--r--plugins/interface/depends.ml (renamed from contrib/interface/depends.ml)0
-rw-r--r--plugins/interface/history.ml (renamed from contrib/interface/history.ml)0
-rw-r--r--plugins/interface/history.mli (renamed from contrib/interface/history.mli)0
-rwxr-xr-xplugins/interface/line_parser.ml4 (renamed from contrib/interface/line_parser.ml4)0
-rw-r--r--plugins/interface/line_parser.mli (renamed from contrib/interface/line_parser.mli)0
-rw-r--r--plugins/interface/name_to_ast.ml (renamed from contrib/interface/name_to_ast.ml)0
-rw-r--r--plugins/interface/name_to_ast.mli (renamed from contrib/interface/name_to_ast.mli)0
-rw-r--r--plugins/interface/paths.ml (renamed from contrib/interface/paths.ml)0
-rw-r--r--plugins/interface/paths.mli (renamed from contrib/interface/paths.mli)0
-rw-r--r--plugins/interface/pbp.ml (renamed from contrib/interface/pbp.ml)0
-rw-r--r--plugins/interface/pbp.mli (renamed from contrib/interface/pbp.mli)0
-rw-r--r--plugins/interface/showproof.ml (renamed from contrib/interface/showproof.ml)0
-rwxr-xr-xplugins/interface/showproof.mli (renamed from contrib/interface/showproof.mli)0
-rw-r--r--plugins/interface/showproof_ct.ml (renamed from contrib/interface/showproof_ct.ml)0
-rw-r--r--plugins/interface/translate.ml (renamed from contrib/interface/translate.ml)0
-rw-r--r--plugins/interface/translate.mli (renamed from contrib/interface/translate.mli)0
-rw-r--r--plugins/interface/vernacrc (renamed from contrib/interface/vernacrc)0
-rw-r--r--plugins/interface/vtp.ml (renamed from contrib/interface/vtp.ml)0
-rw-r--r--plugins/interface/vtp.mli (renamed from contrib/interface/vtp.mli)0
-rw-r--r--plugins/interface/xlate.ml (renamed from contrib/interface/xlate.ml)0
-rw-r--r--plugins/interface/xlate.mli (renamed from contrib/interface/xlate.mli)0
-rw-r--r--plugins/micromega/CheckerMaker.v (renamed from contrib/micromega/CheckerMaker.v)0
-rw-r--r--plugins/micromega/Env.v (renamed from contrib/micromega/Env.v)2
-rw-r--r--plugins/micromega/EnvRing.v (renamed from contrib/micromega/EnvRing.v)0
-rw-r--r--plugins/micromega/LICENSE.sos (renamed from contrib/micromega/LICENSE.sos)0
-rw-r--r--plugins/micromega/MExtraction.v (renamed from contrib/micromega/MExtraction.v)0
-rw-r--r--plugins/micromega/OrderedRing.v (renamed from contrib/micromega/OrderedRing.v)0
-rw-r--r--plugins/micromega/Psatz.v (renamed from contrib/micromega/Psatz.v)0
-rw-r--r--plugins/micromega/QMicromega.v (renamed from contrib/micromega/QMicromega.v)0
-rw-r--r--plugins/micromega/RMicromega.v (renamed from contrib/micromega/RMicromega.v)0
-rw-r--r--plugins/micromega/Refl.v (renamed from contrib/micromega/Refl.v)0
-rw-r--r--plugins/micromega/RingMicromega.v (renamed from contrib/micromega/RingMicromega.v)0
-rw-r--r--plugins/micromega/Tauto.v (renamed from contrib/micromega/Tauto.v)0
-rw-r--r--plugins/micromega/VarMap.v (renamed from contrib/micromega/VarMap.v)4
-rw-r--r--plugins/micromega/ZCoeff.v (renamed from contrib/micromega/ZCoeff.v)0
-rw-r--r--plugins/micromega/ZMicromega.v (renamed from contrib/micromega/ZMicromega.v)0
-rw-r--r--plugins/micromega/certificate.ml (renamed from contrib/micromega/certificate.ml)0
-rw-r--r--plugins/micromega/coq_micromega.ml (renamed from contrib/micromega/coq_micromega.ml)2
-rw-r--r--plugins/micromega/csdpcert.ml (renamed from contrib/micromega/csdpcert.ml)0
-rw-r--r--plugins/micromega/g_micromega.ml4 (renamed from contrib/micromega/g_micromega.ml4)0
-rw-r--r--plugins/micromega/mfourier.ml (renamed from contrib/micromega/mfourier.ml)0
-rw-r--r--plugins/micromega/micromega.ml (renamed from contrib/micromega/micromega.ml)0
-rw-r--r--plugins/micromega/micromega.mli (renamed from contrib/micromega/micromega.mli)0
-rw-r--r--plugins/micromega/micromega_plugin.mllib (renamed from contrib/micromega/micromega_plugin.mllib)0
-rw-r--r--plugins/micromega/mutils.ml (renamed from contrib/micromega/mutils.ml)0
-rw-r--r--plugins/micromega/sos.ml (renamed from contrib/micromega/sos.ml)0
-rw-r--r--plugins/micromega/sos.mli (renamed from contrib/micromega/sos.mli)0
-rw-r--r--plugins/omega/Omega.v (renamed from contrib/omega/Omega.v)0
-rw-r--r--plugins/omega/OmegaLemmas.v (renamed from contrib/omega/OmegaLemmas.v)0
-rw-r--r--plugins/omega/OmegaPlugin.v (renamed from contrib/omega/OmegaPlugin.v)0
-rw-r--r--plugins/omega/PreOmega.v (renamed from contrib/omega/PreOmega.v)0
-rw-r--r--plugins/omega/coq_omega.ml (renamed from contrib/omega/coq_omega.ml)0
-rw-r--r--plugins/omega/g_omega.ml4 (renamed from contrib/omega/g_omega.ml4)0
-rw-r--r--plugins/omega/omega.ml (renamed from contrib/omega/omega.ml)0
-rw-r--r--plugins/omega/omega_plugin.mllib (renamed from contrib/omega/omega_plugin.mllib)0
-rw-r--r--plugins/quote/Quote.v (renamed from contrib/quote/Quote.v)0
-rw-r--r--plugins/quote/g_quote.ml4 (renamed from contrib/quote/g_quote.ml4)0
-rw-r--r--plugins/quote/quote.ml (renamed from contrib/quote/quote.ml)0
-rw-r--r--plugins/quote/quote_plugin.mllib (renamed from contrib/quote/quote_plugin.mllib)0
-rw-r--r--plugins/ring/LegacyArithRing.v (renamed from contrib/ring/LegacyArithRing.v)0
-rw-r--r--plugins/ring/LegacyNArithRing.v (renamed from contrib/ring/LegacyNArithRing.v)0
-rw-r--r--plugins/ring/LegacyRing.v (renamed from contrib/ring/LegacyRing.v)0
-rw-r--r--plugins/ring/LegacyRing_theory.v (renamed from contrib/ring/LegacyRing_theory.v)0
-rw-r--r--plugins/ring/LegacyZArithRing.v (renamed from contrib/ring/LegacyZArithRing.v)0
-rw-r--r--plugins/ring/Ring_abstract.v (renamed from contrib/ring/Ring_abstract.v)0
-rw-r--r--plugins/ring/Ring_normalize.v (renamed from contrib/ring/Ring_normalize.v)0
-rw-r--r--plugins/ring/Setoid_ring.v (renamed from contrib/ring/Setoid_ring.v)0
-rw-r--r--plugins/ring/Setoid_ring_normalize.v (renamed from contrib/ring/Setoid_ring_normalize.v)0
-rw-r--r--plugins/ring/Setoid_ring_theory.v (renamed from contrib/ring/Setoid_ring_theory.v)0
-rw-r--r--plugins/ring/g_ring.ml4 (renamed from contrib/ring/g_ring.ml4)0
-rw-r--r--plugins/ring/ring.ml (renamed from contrib/ring/ring.ml)0
-rw-r--r--plugins/ring/ring_plugin.mllib (renamed from contrib/ring/ring_plugin.mllib)0
-rw-r--r--plugins/romega/README (renamed from contrib/romega/README)0
-rw-r--r--plugins/romega/ROmega.v (renamed from contrib/romega/ROmega.v)0
-rw-r--r--plugins/romega/ReflOmegaCore.v (renamed from contrib/romega/ReflOmegaCore.v)0
-rw-r--r--plugins/romega/const_omega.ml (renamed from contrib/romega/const_omega.ml)0
-rw-r--r--plugins/romega/const_omega.mli (renamed from contrib/romega/const_omega.mli)0
-rw-r--r--plugins/romega/g_romega.ml4 (renamed from contrib/romega/g_romega.ml4)0
-rw-r--r--plugins/romega/refl_omega.ml (renamed from contrib/romega/refl_omega.ml)0
-rw-r--r--plugins/romega/romega_plugin.mllib (renamed from contrib/romega/romega_plugin.mllib)0
-rw-r--r--plugins/rtauto/Bintree.v (renamed from contrib/rtauto/Bintree.v)0
-rw-r--r--plugins/rtauto/Rtauto.v (renamed from contrib/rtauto/Rtauto.v)0
-rw-r--r--plugins/rtauto/g_rtauto.ml4 (renamed from contrib/rtauto/g_rtauto.ml4)0
-rw-r--r--plugins/rtauto/proof_search.ml (renamed from contrib/rtauto/proof_search.ml)0
-rw-r--r--plugins/rtauto/proof_search.mli (renamed from contrib/rtauto/proof_search.mli)0
-rw-r--r--plugins/rtauto/refl_tauto.ml (renamed from contrib/rtauto/refl_tauto.ml)0
-rw-r--r--plugins/rtauto/refl_tauto.mli (renamed from contrib/rtauto/refl_tauto.mli)0
-rw-r--r--plugins/rtauto/rtauto_plugin.mllib (renamed from contrib/rtauto/rtauto_plugin.mllib)0
-rw-r--r--plugins/setoid_ring/ArithRing.v (renamed from contrib/setoid_ring/ArithRing.v)0
-rw-r--r--plugins/setoid_ring/BinList.v (renamed from contrib/setoid_ring/BinList.v)0
-rw-r--r--plugins/setoid_ring/Field.v (renamed from contrib/setoid_ring/Field.v)0
-rw-r--r--plugins/setoid_ring/Field_tac.v (renamed from contrib/setoid_ring/Field_tac.v)0
-rw-r--r--plugins/setoid_ring/Field_theory.v (renamed from contrib/setoid_ring/Field_theory.v)0
-rw-r--r--plugins/setoid_ring/InitialRing.v (renamed from contrib/setoid_ring/InitialRing.v)0
-rw-r--r--plugins/setoid_ring/NArithRing.v (renamed from contrib/setoid_ring/NArithRing.v)0
-rw-r--r--plugins/setoid_ring/RealField.v (renamed from contrib/setoid_ring/RealField.v)0
-rw-r--r--plugins/setoid_ring/Ring.v (renamed from contrib/setoid_ring/Ring.v)0
-rw-r--r--plugins/setoid_ring/Ring_base.v (renamed from contrib/setoid_ring/Ring_base.v)0
-rw-r--r--plugins/setoid_ring/Ring_equiv.v (renamed from contrib/setoid_ring/Ring_equiv.v)0
-rw-r--r--plugins/setoid_ring/Ring_polynom.v (renamed from contrib/setoid_ring/Ring_polynom.v)0
-rw-r--r--plugins/setoid_ring/Ring_tac.v (renamed from contrib/setoid_ring/Ring_tac.v)0
-rw-r--r--plugins/setoid_ring/Ring_theory.v (renamed from contrib/setoid_ring/Ring_theory.v)0
-rw-r--r--plugins/setoid_ring/ZArithRing.v (renamed from contrib/setoid_ring/ZArithRing.v)0
-rw-r--r--plugins/setoid_ring/newring.ml4 (renamed from contrib/setoid_ring/newring.ml4)16
-rw-r--r--plugins/setoid_ring/newring_plugin.mllib (renamed from contrib/setoid_ring/newring_plugin.mllib)0
-rw-r--r--plugins/subtac/equations.ml4 (renamed from contrib/subtac/equations.ml4)0
-rw-r--r--plugins/subtac/eterm.ml (renamed from contrib/subtac/eterm.ml)0
-rw-r--r--plugins/subtac/eterm.mli (renamed from contrib/subtac/eterm.mli)0
-rw-r--r--plugins/subtac/g_eterm.ml4 (renamed from contrib/subtac/g_eterm.ml4)0
-rw-r--r--plugins/subtac/g_subtac.ml4 (renamed from contrib/subtac/g_subtac.ml4)0
-rw-r--r--plugins/subtac/subtac.ml (renamed from contrib/subtac/subtac.ml)0
-rw-r--r--plugins/subtac/subtac.mli (renamed from contrib/subtac/subtac.mli)0
-rw-r--r--plugins/subtac/subtac_cases.ml (renamed from contrib/subtac/subtac_cases.ml)0
-rw-r--r--plugins/subtac/subtac_cases.mli (renamed from contrib/subtac/subtac_cases.mli)0
-rw-r--r--plugins/subtac/subtac_classes.ml (renamed from contrib/subtac/subtac_classes.ml)0
-rw-r--r--plugins/subtac/subtac_classes.mli (renamed from contrib/subtac/subtac_classes.mli)0
-rw-r--r--plugins/subtac/subtac_coercion.ml (renamed from contrib/subtac/subtac_coercion.ml)0
-rw-r--r--plugins/subtac/subtac_coercion.mli (renamed from contrib/subtac/subtac_coercion.mli)0
-rw-r--r--plugins/subtac/subtac_command.ml (renamed from contrib/subtac/subtac_command.ml)0
-rw-r--r--plugins/subtac/subtac_command.mli (renamed from contrib/subtac/subtac_command.mli)0
-rw-r--r--plugins/subtac/subtac_errors.ml (renamed from contrib/subtac/subtac_errors.ml)0
-rw-r--r--plugins/subtac/subtac_errors.mli (renamed from contrib/subtac/subtac_errors.mli)0
-rw-r--r--plugins/subtac/subtac_obligations.ml (renamed from contrib/subtac/subtac_obligations.ml)0
-rw-r--r--plugins/subtac/subtac_obligations.mli (renamed from contrib/subtac/subtac_obligations.mli)0
-rw-r--r--plugins/subtac/subtac_plugin.mllib (renamed from contrib/subtac/subtac_plugin.mllib)0
-rw-r--r--plugins/subtac/subtac_pretyping.ml (renamed from contrib/subtac/subtac_pretyping.ml)0
-rw-r--r--plugins/subtac/subtac_pretyping.mli (renamed from contrib/subtac/subtac_pretyping.mli)0
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml (renamed from contrib/subtac/subtac_pretyping_F.ml)0
-rw-r--r--plugins/subtac/subtac_utils.ml (renamed from contrib/subtac/subtac_utils.ml)0
-rw-r--r--plugins/subtac/subtac_utils.mli (renamed from contrib/subtac/subtac_utils.mli)0
-rw-r--r--plugins/subtac/test/ListDep.v (renamed from contrib/subtac/test/ListDep.v)0
-rw-r--r--plugins/subtac/test/ListsTest.v (renamed from contrib/subtac/test/ListsTest.v)0
-rw-r--r--plugins/subtac/test/Mutind.v (renamed from contrib/subtac/test/Mutind.v)0
-rw-r--r--plugins/subtac/test/Test1.v (renamed from contrib/subtac/test/Test1.v)0
-rw-r--r--plugins/subtac/test/euclid.v (renamed from contrib/subtac/test/euclid.v)0
-rw-r--r--plugins/subtac/test/id.v (renamed from contrib/subtac/test/id.v)0
-rw-r--r--plugins/subtac/test/measure.v (renamed from contrib/subtac/test/measure.v)0
-rw-r--r--plugins/subtac/test/rec.v (renamed from contrib/subtac/test/rec.v)0
-rw-r--r--plugins/subtac/test/take.v (renamed from contrib/subtac/test/take.v)0
-rw-r--r--plugins/subtac/test/wf.v (renamed from contrib/subtac/test/wf.v)0
-rw-r--r--plugins/xml/COPYRIGHT (renamed from contrib/xml/COPYRIGHT)0
-rw-r--r--plugins/xml/README (renamed from contrib/xml/README)0
-rw-r--r--plugins/xml/acic.ml (renamed from contrib/xml/acic.ml)0
-rw-r--r--plugins/xml/acic2Xml.ml4 (renamed from contrib/xml/acic2Xml.ml4)0
-rw-r--r--plugins/xml/cic.dtd (renamed from contrib/xml/cic.dtd)0
-rw-r--r--plugins/xml/cic2Xml.ml (renamed from contrib/xml/cic2Xml.ml)0
-rw-r--r--plugins/xml/cic2acic.ml (renamed from contrib/xml/cic2acic.ml)0
-rw-r--r--plugins/xml/doubleTypeInference.ml (renamed from contrib/xml/doubleTypeInference.ml)0
-rw-r--r--plugins/xml/doubleTypeInference.mli (renamed from contrib/xml/doubleTypeInference.mli)0
-rw-r--r--plugins/xml/dumptree.ml4 (renamed from contrib/xml/dumptree.ml4)0
-rw-r--r--plugins/xml/proof2aproof.ml (renamed from contrib/xml/proof2aproof.ml)0
-rw-r--r--plugins/xml/proofTree2Xml.ml4 (renamed from contrib/xml/proofTree2Xml.ml4)0
-rw-r--r--plugins/xml/theoryobject.dtd (renamed from contrib/xml/theoryobject.dtd)0
-rw-r--r--plugins/xml/unshare.ml (renamed from contrib/xml/unshare.ml)0
-rw-r--r--plugins/xml/unshare.mli (renamed from contrib/xml/unshare.mli)0
-rw-r--r--plugins/xml/xml.ml4 (renamed from contrib/xml/xml.ml4)0
-rw-r--r--plugins/xml/xml.mli (renamed from contrib/xml/xml.mli)0
-rw-r--r--plugins/xml/xml_plugin.mllib (renamed from contrib/xml/xml_plugin.mllib)0
-rw-r--r--plugins/xml/xmlcommand.ml (renamed from contrib/xml/xmlcommand.ml)0
-rw-r--r--plugins/xml/xmlcommand.mli (renamed from contrib/xml/xmlcommand.mli)0
-rw-r--r--plugins/xml/xmlentries.ml4 (renamed from contrib/xml/xmlentries.ml4)0
-rw-r--r--tools/coq_makefile.ml42
-rw-r--r--tools/coqdep.ml4
-rw-r--r--tools/coqdep_boot.ml6
-rw-r--r--toplevel/coqinit.ml4
301 files changed, 169 insertions, 170 deletions
diff --git a/CHANGES b/CHANGES
index df2783349..dc7efbab3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1023,7 +1023,7 @@ Tactics
- Clear now fails when trying to remove a local definition used by
a constant appearing in the current goal
-Extraction (See details in contrib/extraction/CHANGES)
+Extraction (See details in plugins/extraction/CHANGES)
- The old commands: (Recursive) Extraction Module M.
are now: (Recursive) Extraction Library M.
@@ -1163,7 +1163,7 @@ Tactics
- Unfold expects a correct evaluable argument
- Clear expects existing hypotheses
-Extraction (See details in contrib/extraction/CHANGES and README):
+Extraction (See details in plugins/extraction/CHANGES and README):
- An experimental Scheme extraction is provided.
- Concerning Ocaml, extracted code is now ensured to always type-check,
@@ -1278,7 +1278,7 @@ Bugs
- Known bugs related to Inversion and let-in's fixed
- Bug unexpected Delta with let-in now fixed
-Extraction (details in contrib/extraction/CHANGES or documentation)
+Extraction (details in plugins/extraction/CHANGES or documentation)
- Signatures of extracted terms are now mostly expunged from dummy arguments.
- Haskell extraction is now operational (tested & debugged).
@@ -1286,7 +1286,7 @@ Extraction (details in contrib/extraction/CHANGES or documentation)
Standard library
- Some additions in [ZArith]: three files (Zcomplements.v, Zpower.v
- and Zlogarithms.v) moved from contrib/omega in order to be more
+ and Zlogarithms.v) moved from plugins/omega in order to be more
visible, one Zsgn function, more induction principles (Wf_Z.v and
tail of Zcomplements.v), one more general Euclid theorem
- Peano_dec.v and Compare_dec.v now part of Arith.v
@@ -1349,7 +1349,7 @@ Tactics
- Slight improvement in naming strategy for NewInduction/NewDestruct
- Intuition/Tauto do not perform useless unfolding and work up to conversion
-Extraction (details in contrib/extraction/CHANGES or documentation)
+Extraction (details in plugins/extraction/CHANGES or documentation)
- Syntax changes: there are no more options inside the extraction commands.
New commands for customization and options have been introduced instead.
diff --git a/COPYRIGHT b/COPYRIGHT
index 7ed31f15d..63d905739 100644
--- a/COPYRIGHT
+++ b/COPYRIGHT
@@ -13,12 +13,12 @@ work time rest with the employee. By analogy, it is Lionel's opinion
that copyright on these changes rests with him.
This product includes also software developed by
- Yves Bertot, Lemme, INRIA Sophia-Antipolis (contrib/interface,
+ Yves Bertot, Lemme, INRIA Sophia-Antipolis (plugins/interface,
parsing/search.ml)
- Pierre Crégut, France Telecom R & D (contrib/omega and contrib/romega)
- Pierre Courtieu, Lemme (contrib/funind)
- Loïc Pottier, Lemme, INRIA Sophia-Antipolis (contrib/fourier)
- Claudio Sacerdoti Coen, HELM, University of Bologna, (contrib/xml)
+ Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega)
+ Pierre Courtieu, Lemme (plugins/funind)
+ Loïc Pottier, Lemme, INRIA Sophia-Antipolis (plugins/fourier)
+ Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml)
The file CREDITS contains a list of past contributors
The credits section in Reference Manual introduction details
diff --git a/CREDITS b/CREDITS
index b3d563caf..c982d6724 100644
--- a/CREDITS
+++ b/CREDITS
@@ -23,53 +23,53 @@ The following directories contain independent contributions supported
by the Coq development team. All of them are released under the terms of
the GNU Lesser General Public License Version 2.1.
-contrib/cc
+plugins/cc
developed by Pierre Corbineau (ENS Cachan, 2001, LRI, 2001-2005, Radboud
University at Nijmegen, 2005-2008)
-contrib/correctness
+plugins/correctness
developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
-contrib/dp
+plugins/dp
developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre
(LRI, 2005-2008)
-contrib/extraction
+plugins/extraction
developed by Pierre Letouzey (LRI, 2000-2004, PPS-Paris7, 2005-now)
-contrib/field
+plugins/field
developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
-contrib/firstorder
+plugins/firstorder
developed by Pierre Corbineau (LRI, 2003-2008)
-contrib/fourier
+plugins/fourier
developed by Loïc Pottier (INRIA-Lemme, 2001)
-contrib/funind
+plugins/funind
developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2008),
Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008)
and Yves Bertot (INRIA-Marelle, 2005-2006)
-contrib/interface
+plugins/interface
developed by Yves Bertot with contributions from Loïc Pottier and
Laurence Rideau as part of the Pcoq project (INRIA-Lemme, 1997-2006);
extended by Lionel Mamane as part of the TeXMacs project (Radboud university
at Nijmegen, 2007-2008)
-contrib/omega
+plugins/omega
developed by Pierre Crégut (France Telecom R&D, 1996)
-contrib/recdef
+plugins/recdef
developed by Yves Bertot (INRIA-Marelle, 2005-2006)
-contrib/ring
+plugins/ring
developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick
Loiseleur (LRI, 1997-1999)
-contrib/romega
+plugins/romega
developed by Pierre Crégut (France Telecom R&D, 2001-2004)
-contrib/rtauto
+plugins/rtauto
developed by Pierre Corbineau (LRI, 2005)
-contrib/setoid_ring
+plugins/setoid_ring
developed by Benjamin Grégoire (INRIA-Everest, 2005-2006),
Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006)
and Bruno Barras (INRIA LogiCal, 2005-2006),
-contrib/subtac
+plugins/subtac
developed by Matthieu Sozeau (LRI, 2005-2008)
-contrib/xml
+plugins/xml
developed by Claudio Sacerdoti (Univ. Bologna, 2000-2005)
as part of the HELM and MoWGLI projects; extension by Cezary Kaliszyk as
part of the ProofWeb project (Radbout University at Nijmegen, 2008)
-contrib/micromega
+plugins/micromega
developed by Frédéric Besson (IRISA/INRIA, 2006-2008), with some
extensions by Evgeny Makarov (INRIA, 2007); sum-of-squares solver and
interface to the csdp solver uses code from John Harrison (University
diff --git a/Makefile b/Makefile
index 1413d0faa..e8f5fabfe 100644
--- a/Makefile
+++ b/Makefile
@@ -196,8 +196,8 @@ indepclean:
rm -f bin/coq-interface$(EXE) bin/coq-parser$(EXE)
find . -name '*~' -or -name '*.cm[ioa]' | xargs rm -f
find . -name '*_mod.ml' | xargs rm -f
- find contrib test-suite -name '*.vo' -or -name '*.glob' | xargs rm -f
- rm -f */*.pp[iox] contrib/*/*.pp[iox]
+ find plugins test-suite -name '*.vo' -or -name '*.glob' | xargs rm -f
+ rm -f */*.pp[iox] plugins/*/*.pp[iox]
rm -rf $(SOURCEDOCDIR)
rm -f toplevel/mltop.byteml toplevel/mltop.optml
rm -f test-suite/check.log
diff --git a/Makefile.build b/Makefile.build
index a3298230c..dd27cfcbd 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -156,7 +156,7 @@ coqbinaries:: ${COQBINARIES} ${CSDPCERT}
coq: coqlib tools coqbinaries
-coqlib:: theories contrib
+coqlib:: theories plugins
coqlight: theories-light tools coqbinaries
@@ -278,11 +278,11 @@ parsing/highparsing.cmxa: $(HIGHPARSING:.cmo=.cmx)
tactics/hightactics.cma: $(HIGHTACTICS)
tactics/hightactics.cmxa: $(HIGHTACTICS:.cmo=.cmx)
-contrib/%.cma: | contrib/%.mllib.d
+plugins/%.cma: | plugins/%.mllib.d
$(SHOW)'OCAMLC -a -o $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^
-contrib/%.cmxa: | contrib/%.mllib.d
+plugins/%.cmxa: | plugins/%.mllib.d
$(SHOW)'OCAMLOPT -a -o $@'
$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^
@@ -309,12 +309,12 @@ checker/check.cmxa: $(MCHECKER:.cmo=.cmx)
###########################################################################
ifeq ($(BEST),opt)
-contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMX)
+plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMX)
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa -o $@ $^
$(STRIP) $@
else
-contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMO)
+plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma -o $@ $^
endif
@@ -453,8 +453,8 @@ install-pcoq-binaries::
$(INSTALLBIN) $(COQINTERFACE) $(FULLBINDIR)
install-pcoq-files::
- $(MKDIR) $(FULLCOQLIB)/contrib/interface
- $(INSTALLLIB) $(PCOQFILES) $(FULLCOQLIB)/contrib/interface
+ $(MKDIR) $(FULLCOQLIB)/plugins/interface
+ $(INSTALLLIB) $(PCOQFILES) $(FULLCOQLIB)/plugins/interface
install-pcoq-manpages:
$(MKDIR) $(FULLMANDIR)/man1
@@ -467,7 +467,7 @@ install-pcoq-manpages:
VALIDOPTS=-silent -o -m
validate:: $(BESTCHICKEN) $(ALLVO)
- $(SHOW)'COQCHK <theories & contrib>'
+ $(SHOW)'COQCHK <theories & plugins>'
$(HIDE)$(BESTCHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
check:: world validate
@@ -476,7 +476,7 @@ check:: world validate
if grep -F 'Error!' test-suite/check.log ; then false; fi
###########################################################################
-# theories and contrib files
+# theories and plugins files
###########################################################################
init: $(INITVO)
@@ -512,10 +512,10 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \
wellfounded setoids sorting
###########################################################################
-# contribs (interface not included)
+# plugins (interface not included)
###########################################################################
-contrib: $(CONTRIBVO)
+plugins: $(PLUGINSVO)
omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT)
ring: $(RINGVO) $(RINGCMA)
@@ -531,7 +531,7 @@ subtac: $(SUBTACCMA)
rtauto: $(RTAUTOVO) $(RTAUTOCMA)
###########################################################################
-# rules to make theories, contrib and states
+# rules to make theories, plugins and states
###########################################################################
states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_STRICT) | states/MakeInitial.v.d $(VO_TOOLS_ORDER_ONLY)
@@ -690,8 +690,8 @@ ifeq ($(BEST),opt)
endif
# csdpcert is not meant to be directly called by the user; we install
# it with libraries
- -$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega
- $(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/contrib/micromega
+ -$(MKDIR) -p $(FULLCOQLIB)/plugins/micromega
+ $(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/plugins/micromega
-$(INSTALLLIB) revision $(FULLCOQLIB)
install-library-light:
diff --git a/Makefile.common b/Makefile.common
index 0fc205b2d..b8462539d 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -58,14 +58,14 @@ COQBINARIES:= $(COQMKTOP) $(COQC) \
endif
OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)
-CSDPCERT:=contrib/micromega/csdpcert$(EXE)
+CSDPCERT:=plugins/micromega/csdpcert$(EXE)
SRCDIRS:=\
config tools tools/coqdoc scripts lib \
kernel kernel/byterun library proofs tactics \
pretyping interp toplevel parsing ide/utils \
ide \
- $(addprefix contrib/, \
+ $(addprefix plugins/, \
omega romega micromega quote ring dp \
setoid_ring xml extraction interface fourier \
cc funind firstorder field subtac \
@@ -241,44 +241,44 @@ HIGHTACTICS:=$(addprefix tactics/, \
eauto.cmo class_tactics.cmo tauto.cmo \
eqdecide.cmo )
-# NB: Dependencies of contribs are now in separate files
-# contrib/*/*_plugin.mllib
+# NB: Dependencies of plugins are now in separate files
+# plugins/*/*_plugin.mllib
# Format of these files are compatible with ocamlbuild,
# Even if we don't use it (yet ?)
-OMEGACMA:=contrib/omega/omega_plugin.cma
-ROMEGACMA:=contrib/romega/romega_plugin.cma
-MICROMEGACMA:=contrib/micromega/micromega_plugin.cma
-QUOTECMA:=contrib/quote/quote_plugin.cma
-RINGCMA:=contrib/ring/ring_plugin.cma
-NEWRINGCMA:=contrib/setoid_ring/newring_plugin.cma
-GBCMA:=contrib/groebner/groebner_plugin.cma
-DPCMA:=contrib/dp/dp_plugin.cma
-FIELDCMA:=contrib/field/field_plugin.cma
-XMLCMA:=contrib/xml/xml_plugin.cma
-FOURIERCMA:=contrib/fourier/fourier_plugin.cma
-EXTRACTIONCMA:=contrib/extraction/extraction_plugin.cma
-FUNINDCMA:=contrib/funind/recdef_plugin.cma
-FOCMA:=contrib/firstorder/ground_plugin.cma
-CCCMA:=contrib/cc/cc_plugin.cma
-SUBTACCMA:=contrib/subtac/subtac_plugin.cma
-RTAUTOCMA:=contrib/rtauto/rtauto_plugin.cma
-
-CONTRIBS:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \
+OMEGACMA:=plugins/omega/omega_plugin.cma
+ROMEGACMA:=plugins/romega/romega_plugin.cma
+MICROMEGACMA:=plugins/micromega/micromega_plugin.cma
+QUOTECMA:=plugins/quote/quote_plugin.cma
+RINGCMA:=plugins/ring/ring_plugin.cma
+NEWRINGCMA:=plugins/setoid_ring/newring_plugin.cma
+GBCMA:=plugins/groebner/groebner_plugin.cma
+DPCMA:=plugins/dp/dp_plugin.cma
+FIELDCMA:=plugins/field/field_plugin.cma
+XMLCMA:=plugins/xml/xml_plugin.cma
+FOURIERCMA:=plugins/fourier/fourier_plugin.cma
+EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cma
+FUNINDCMA:=plugins/funind/recdef_plugin.cma
+FOCMA:=plugins/firstorder/ground_plugin.cma
+CCCMA:=plugins/cc/cc_plugin.cma
+SUBTACCMA:=plugins/subtac/subtac_plugin.cma
+RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma
+
+PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \
$(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \
$(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \
$(CCCMA) $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \
$(FUNINDCMA) $(GBCMA)
ifneq ($(HASNATDYNLINK),false)
- CONTRIBSTATIC:=
+ STATICPLUGINS:=
INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \
$(XMLCMA) $(FUNINDCMA) $(SUBTACCMA)
INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
- PLUGINS:=$(CONTRIBS)
- PLUGINSOPT:=$(PLUGINS:.cma=.cmxs)
+ PLUGINS:=$(PLUGINSCMA)
+ PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
else
- CONTRIBSTATIC:=$(CONTRIBS)
+ STATICPLUGINS:=$(PLUGINSCMA)
INITPLUGINS:=
INITPLUGINSOPT:=
PLUGINS:=
@@ -296,7 +296,7 @@ CMXA:=$(CMA:.cma=.cmxa)
LINKCMO:=$(CONFIG) lib/lib.cma kernel/kernel.cma library/library.cma \
pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \
- parsing/highparsing.cma tactics/hightactics.cma $(CONTRIBSTATIC)
+ parsing/highparsing.cma tactics/hightactics.cma $(STATICPLUGINS)
LINKCMX:=$(patsubst %.cma,%.cmxa,$(patsubst %.cmo,%.cmx,$(LINKCMO)))
# objects known by the toplevel of Coq
@@ -332,17 +332,17 @@ COQCCMX:=$(COQCCMO:.cmo=.cmx)
COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-parser$(EXE)
-INTERFACECMA:=contrib/interface/coqinterface_plugin.cma
-PARSERCMA:=contrib/interface/coqparser_plugin.cma
+INTERFACECMA:=plugins/interface/coqinterface_plugin.cma
+PARSERCMA:=plugins/interface/coqparser_plugin.cma
ifeq ($(HASNATDYNLINK),false)
ifeq ($(BEST),opt)
COQINTERFACE:=$(COQINTERFACE) bin/coq-interface.opt$(EXE) bin/coq-parser.opt$(EXE)
endif
- INTERFACERC:= contrib/interface/vernacrc
+ INTERFACERC:= plugins/interface/vernacrc
PCOQPLUGINS:=
else
- INTERFACERC:= contrib/interface/vernacrc contrib/interface/CoqParser.v
+ INTERFACERC:= plugins/interface/vernacrc plugins/interface/CoqParser.v
PCOQPLUGINS:=$(INTERFACECMA) $(PARSERCMA)
endif
@@ -351,7 +351,7 @@ PARSERREQUIRESCMX:=$(LINKCMX) $(PARSERCMA:.cma=.cmxa)
## Misc
-CSDPCERTCMO:=$(addprefix contrib/micromega/, \
+CSDPCERTCMO:=$(addprefix plugins/micromega/, \
mutils.cmo micromega.cmo mfourier.cmo certificate.cmo \
sos.cmo csdpcert.cmo )
CSDPCERTCMX:= $(CSDPCERTCMO:.cmo=.cmx)
@@ -687,15 +687,15 @@ THEORIESVO:=\
THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO)
-## Contribs
+## Plugins
-OMEGAVO:=$(addprefix contrib/omega/, \
+OMEGAVO:=$(addprefix plugins/omega/, \
PreOmega.vo OmegaLemmas.vo OmegaPlugin.vo Omega.vo )
-ROMEGAVO:=$(addprefix contrib/romega/, \
+ROMEGAVO:=$(addprefix plugins/romega/, \
ReflOmegaCore.vo ROmega.vo )
-MICROMEGAVO:=$(addprefix contrib/micromega/, \
+MICROMEGAVO:=$(addprefix plugins/micromega/, \
CheckerMaker.vo Refl.vo \
Env.vo RingMicromega.vo \
EnvRing.vo VarMap.vo \
@@ -704,10 +704,10 @@ MICROMEGAVO:=$(addprefix contrib/micromega/, \
QMicromega.vo RMicromega.vo \
Tauto.vo )
-QUOTEVO:=$(addprefix contrib/quote/, \
+QUOTEVO:=$(addprefix plugins/quote/, \
Quote.vo )
-RINGVO:=$(addprefix contrib/ring/, \
+RINGVO:=$(addprefix plugins/ring/, \
LegacyArithRing.vo Ring_normalize.vo \
LegacyRing_theory.vo LegacyRing.vo \
LegacyNArithRing.vo \
@@ -715,11 +715,11 @@ RINGVO:=$(addprefix contrib/ring/, \
Setoid_ring_normalize.vo \
Setoid_ring.vo Setoid_ring_theory.vo )
-FIELDVO:=$(addprefix contrib/field/, \
+FIELDVO:=$(addprefix plugins/field/, \
LegacyField_Compl.vo LegacyField_Theory.vo \
LegacyField_Tactic.vo LegacyField.vo )
-NEWRINGVO:=$(addprefix contrib/setoid_ring/, \
+NEWRINGVO:=$(addprefix plugins/setoid_ring/, \
BinList.vo Ring_theory.vo \
Ring_polynom.vo Ring_tac.vo \
Ring_base.vo InitialRing.vo \
@@ -729,48 +729,48 @@ NEWRINGVO:=$(addprefix contrib/setoid_ring/, \
Field_theory.vo Field_tac.vo \
Field.vo RealField.vo )
-GBVO:=$(addprefix contrib/groebner/, \
+GBVO:=$(addprefix plugins/groebner/, \
GroebnerR.vo GroebnerZ.vo )
XMLVO:=
-FOURIERVO:=$(addprefix contrib/fourier/, \
+FOURIERVO:=$(addprefix plugins/fourier/, \
Fourier_util.vo Fourier.vo )
FUNINDVO:=
-RECDEFVO:=$(addprefix contrib/funind/, \
+RECDEFVO:=$(addprefix plugins/funind/, \
Recdef.vo )
CCVO:=
-DPVO:=$(addprefix contrib/dp/, \
+DPVO:=$(addprefix plugins/dp/, \
Dp.vo )
-RTAUTOVO:=$(addprefix contrib/rtauto/, \
+RTAUTOVO:=$(addprefix plugins/rtauto/, \
Bintree.vo Rtauto.vo )
ifneq ($(HASNATDYNLINK),false)
-INTERFACEVO:=contrib/interface/CoqInterface.vo
+INTERFACEVO:=plugins/interface/CoqInterface.vo
else
INTERFACEVO:=
endif
-CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
+PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
$(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \
$(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \
$(INTERFACEVO) $(GBVO)
-ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO)
+ALLVO:= $(INITVO) $(THEORIESVO) $(PLUGINSVO)
VFILES:= $(ALLVO:.vo=.v)
# convert a (stdlib) filename into a module name:
-# remove .vo, replace theories and contrib by Coq, and replace slashes by dots
-vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst contrib/%,Coq.%,$(1:.vo=))))
+# remove .vo, replace theories and plugins by Coq, and replace slashes by dots
+vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
ALLMODS:=$(call vo_to_mod,$(ALLVO))
-LIBFILES:=$(THEORIESVO) $(CONTRIBVO)
+LIBFILES:=$(THEORIESVO) $(PLUGINSVO)
LIBFILESLIGHT:=$(THEORIESLIGHTVO)
## Specials
@@ -839,7 +839,7 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
pcoq-binaries $(COQINTERFACE) $(CSDPCERT) coqbinaries pcoq $(TOOLS) tools \
printers debug initplugins plugins \
world install coqide coqide-files coq coqlib \
- coqlight states pcoq-files check init theories theories-light contrib \
+ coqlight states pcoq-files check init theories theories-light \
$(DOC_TARGETS) $(VO_TARGETS) validate \
%.vo %.glob states/% install-% %.ml4-preprocessed
diff --git a/Makefile.doc b/Makefile.doc
index cf849dadf..e5822eb5b 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -49,7 +49,7 @@ ifdef QUICK
%.v.tex: %.tex
(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
else
-%.v.tex: %.tex | $(COQTEX) $(COQTOPEXE) $(CONTRIBVO) $(THEORIESVO)
+%.v.tex: %.tex | $(COQTEX) $(COQTOPEXE) $(PLUGINSVO) $(THEORIESVO)
(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
endif
diff --git a/checker/checker.ml b/checker/checker.ml
index 70e2eb97f..b982456aa 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -113,12 +113,12 @@ let set_rec_include d p =
let init_load_path () =
let coqlib = Envars.coqlib () in
let user_contrib = coqlib/"user-contrib" in
- let contrib = coqlib/"contrib" in
+ let plugins = coqlib/"plugins" in
(* first user-contrib *)
if Sys.file_exists user_contrib then
add_rec_path user_contrib Check.default_root_prefix;
- (* then contrib *)
- add_rec_path contrib (Names.make_dirpath [coq_root]);
+ (* then plugins *)
+ add_rec_path plugins (Names.make_dirpath [coq_root]);
(* then standard library *)
(* List.iter
(fun (s,alias) ->
diff --git a/config/coq_config.mli b/config/coq_config.mli
index b5ccbbca7..7c80a96d4 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -36,7 +36,7 @@ val vo_magic_number : int
val state_magic_number : int
val theories_dirs : string list
-val contrib_dirs : string list
+val plugins_dirs : string list
val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof with Coqide *)
diff --git a/configure b/configure
index de3c6fbbd..1e9dc472f 100755
--- a/configure
+++ b/configure
@@ -972,8 +972,8 @@ echo "let theories_dirs = [" >> "$mlconfig_file"
subdirs theories
echo "]" >> "$mlconfig_file"
-echo "let contrib_dirs = [" >> "$mlconfig_file"
-subdirs contrib
+echo "let plugins_dirs = [" >> "$mlconfig_file"
+subdirs plugins
echo "]" >> "$mlconfig_file"
chmod a-w "$mlconfig_file"
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 5aadfa592..a9673664a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -344,7 +344,7 @@ Proof_type: subproof field in type proof_tree glued with the ref field
Tacmach: no more echo from functions of module Refiner
-Files contrib/*/g_*.ml4 take the place of files contrib/*/*.v.
+Files plugins/*/g_*.ml4 take the place of files plugins/*/*.v.
Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd
VERNAC COMMAND EXTEND macros
File syntax/PPTactic.v moved to parsing/pptactic.ml
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 560d06d96..2598d6df1 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -17,13 +17,13 @@ exec $OCAMLDEBUG \
-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
-I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \
-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
- -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \
- -I $COQTOP/contrib/fourier -I $COQTOP/contrib/firstorder \
- -I $COQTOP/contrib/interface \
- -I $COQTOP/contrib/omega -I $COQTOP/contrib/romega \
- -I $COQTOP/contrib/ring -I $COQTOP/contrib/xml \
- -I $COQTOP/contrib/subtac -I $COQTOP/contrib/funind \
- -I $COQTOP/contrib/rtauto -I $COQTOP/contrib/setoid_ring \
- -I $COQTOP/contrib/recdef -I $COQTOP/contrib/dp \
+ -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
+ -I $COQTOP/plugins/fourier -I $COQTOP/plugins/firstorder \
+ -I $COQTOP/plugins/interface \
+ -I $COQTOP/plugins/omega -I $COQTOP/plugins/romega \
+ -I $COQTOP/plugins/ring -I $COQTOP/plugins/xml \
+ -I $COQTOP/plugins/subtac -I $COQTOP/plugins/funind \
+ -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \
+ -I $COQTOP/plugins/recdef -I $COQTOP/plugins/dp \
-I $COQTOP/ide \
$*
diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile
index f2c625ed4..8ad226da6 100644
--- a/dev/ocamlweb-doc/Makefile
+++ b/dev/ocamlweb-doc/Makefile
@@ -4,14 +4,14 @@ LOCALINCLUDES=-I ../../config -I ../../tools -I ../../tools/coqdoc \
-I ../../scripts -I ../../lib -I ../../kernel -I ../../kernel/byterun -I ../../library \
-I ../../proofs -I ../../tactics -I ../../pretyping \
-I ../../interp -I ../../toplevel -I ../../parsing -I ../../ide/utils -I ../../ide \
- -I ../../contrib/omega -I ../../contrib/romega \
- -I ../../contrib/ring -I ../../contrib/dp -I ../../contrib/setoid_ring \
- -I ../../contrib/xml -I ../../contrib/extraction \
- -I ../../contrib/interface -I ../../contrib/fourier \
- -I ../../contrib/cc \
- -I ../../contrib/funind -I ../../contrib/firstorder \
- -I ../../contrib/field -I ../../contrib/subtac -I ../../contrib/rtauto \
- -I ../../contrib/recdef
+ -I ../../plugins/omega -I ../../plugins/romega \
+ -I ../../plugins/ring -I ../../plugins/dp -I ../../plugins/setoid_ring \
+ -I ../../plugins/xml -I ../../plugins/extraction \
+ -I ../../plugins/interface -I ../../plugins/fourier \
+ -I ../../plugins/cc \
+ -I ../../plugins/funind -I ../../plugins/firstorder \
+ -I ../../plugins/field -I ../../plugins/subtac -I ../../plugins/rtauto \
+ -I ../../plugins/recdef
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index de68ce1e5..46ba24da7 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -744,28 +744,28 @@ Conflicts exists between integers and constrs.
\nlsep \TERM{simplif}
\nlsep \TERM{intuition}~\OPT{\NTL{tactic}{0}}
\nlsep \TERM{linearintuition}~\OPT{\NT{num}}
-%% contrib/cc
+%% plugins/cc
\nlsep \TERM{cc}
-%% contrib/field
+%% plugins/field
\nlsep \TERM{field}~\STAR{\tacconstr}
-%% contrib/firstorder
+%% plugins/firstorder
\nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}
\nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{with}~\PLUS{\NT{reference}}
\nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{using}~\PLUS{\NT{ident}}
%%\nlsep \TERM{gtauto}
\nlsep \TERM{gintuition}~\OPT{\NTL{tactic}{0}}
-%% contrib/fourier
+%% plugins/fourier
\nlsep \TERM{fourierZ}
-%% contrib/funind
+%% plugins/funind
\nlsep \TERM{functional}~\TERM{induction}~\tacconstr~\PLUS{\tacconstr}
-%% contrib/jprover
+%% plugins/jprover
\nlsep \TERM{jp}~\OPT{\NT{num}}
-%% contrib/omega
+%% plugins/omega
\nlsep \TERM{omega}
-%% contrib/ring
+%% plugins/ring
\nlsep \TERM{quote}~\NT{ident}~\OPTGR{\KWD{[}~\PLUS{\NT{ident}}~\KWD{]}}
\nlsep \TERM{ring}~\STAR{\tacconstr}
-%% contrib/romega
+%% plugins/romega
\nlsep \TERM{romega}
\SEPDEF
\DEFNT{orient}
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 4309926b9..baf3d4991 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -1983,7 +1983,7 @@ todo
\Question{Can you show me an example of a tactic written in OCaml?}
-You have some examples of tactics written in Ocaml in the ``contrib'' directory of {\Coq} sources.
+You have some examples of tactics written in Ocaml in the ``plugins'' directory of {\Coq} sources.
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index ba07182a6..8271c7c32 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -620,7 +620,7 @@ quite efficient for Caml code.
As a test, we propose an automatic extraction of the
Standard Library of \Coq. In particular, we will find back the
two previous examples, {\tt Euclid} and {\tt Heapsort}.
-Go to directory {\tt contrib/extraction/test} of the sources of \Coq,
+Go to directory {\tt plugins/extraction/test} of the sources of \Coq,
and run commands:
\begin{verbatim}
make tree; make
@@ -653,7 +653,7 @@ also work, just adapt the {\tt Makefile.haskell}. In particular {\tt
Some pathological examples of extraction are grouped in the file
\begin{verbatim}
-contrib/extraction/test_extraction.v
+plugins/extraction/test_extraction.v
\end{verbatim}
of the sources of \Coq.
diff --git a/doc/refman/Helm.tex b/doc/refman/Helm.tex
index d07b1204c..74db9c86d 100644
--- a/doc/refman/Helm.tex
+++ b/doc/refman/Helm.tex
@@ -273,7 +273,7 @@ of the calculus is also proved.
\subsubsection{The CIC with Explicit Named Substitutions XML DTD}
A copy of the DTD can be found in the file ``\verb+cic.dtd+'' in the
-\verb+contrib/xml+ source directory of \Coq.
+\verb+plugins/xml+ source directory of \Coq.
The following is a very brief overview of the elements described in the DTD.
\begin{description}
diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
index 48937113f..94c76c197 100644
--- a/doc/refman/Polynom.tex
+++ b/doc/refman/Polynom.tex
@@ -336,21 +336,21 @@ describes their syntax and effects:
evaluation function of power coefficient) is the original term, or
returns {\tt InitialRing.NotConstant} if not a constant coefficient
(i.e. {\ltac} is the inverse function of {\tt Cp\_phi}).
- See files {\tt contrib/setoid\_ring/ZArithRing.v} and
- {\tt contrib/setoid\_ring/RealField.v} for examples.
+ See files {\tt plugins/setoid\_ring/ZArithRing.v} and
+ {\tt plugins/setoid\_ring/RealField.v} for examples.
By default the tactic does not recognize power expressions as ring
expressions.
\item[sign {\term}] allows {\tt ring\_simplify} to use a minus operation
when outputing its normal form, i.e writing $x - y$ instead of $x + (-y)$.
The term {\term} is a proof that a given sign function indicates expressions
that are signed ({\term} has to be a
- proof of {\tt Ring\_theory.get\_sign}). See {\tt contrib/setoid\_ring/IntialRing.v} for examples of sign function.
+ proof of {\tt Ring\_theory.get\_sign}). See {\tt plugins/setoid\_ring/IntialRing.v} for examples of sign function.
\item[div {\term}] allows {\tt ring} and {\tt ring\_simplify} to use moniomals
with coefficient other than 1 in the rewriting. The term {\term} is a proof that a given division function satisfies the specification of an euclidean
division function ({\term} has to be a
proof of {\tt Ring\_theory.div\_theory}). For example, this function is
called when trying to rewrite $7x$ by $2x = z$ to tell that $7 = 3 * 2 + 1$.
- See {\tt contrib/setoid\_ring/IntialRing.v} for examples of div function.
+ See {\tt plugins/setoid\_ring/IntialRing.v} for examples of div function.
\end{description}
@@ -490,7 +490,7 @@ constants can be proven different from zero automatically.
The tactic must be loaded by \texttt{Require Import Field}. New field
structures can be declared to the system with the \texttt{Add Field}
command (see below). The field of real numbers is defined in module
-\texttt{RealField} (in texttt{contrib/setoid\_ring}). It is exported
+\texttt{RealField} (in texttt{plugins/setoid\_ring}). It is exported
by module \texttt{Rbase}, so that requiring \texttt{Rbase} or
\texttt{Reals} is enough to use the field tactics on real
numbers. Rational numbers in canonical form are also declared as a
@@ -696,7 +696,7 @@ the file
\begin{quotation}
\begin{verbatim}
-contrib/ring/Ring_theory.v
+plugins/ring/Ring_theory.v
\end{verbatim}
\end{quotation}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9ed2e650c..4e31137c9 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3565,7 +3565,7 @@ intros; field.
Reset Initial.
\end{coq_eval}
-\SeeAlso file {\tt contrib/setoid\_ring/RealField.v} for an example of instantiation,\\
+\SeeAlso file {\tt plugins/setoid\_ring/RealField.v} for an example of instantiation,\\
\phantom{\SeeAlso}theory {\tt theories/Reals} for many examples of use of {\tt
field}.
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index dbd863469..9af44115a 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -1084,7 +1084,7 @@ is undecidable in general case, don't expect miracles from it!
% \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v}
-\SeeAlso comments of source file \texttt{tactics/contrib/polynom/quote.ml}
+\SeeAlso comments of source file \texttt{plugins/quote/quote.ml}
\SeeAlso the \texttt{ring} tactic (Chapter~\ref{ring})
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
index d7239c8fd..5a3ccda6a 100644
--- a/doc/refman/RefMan-tus.tex
+++ b/doc/refman/RefMan-tus.tex
@@ -1186,8 +1186,7 @@ function body or behind the \texttt{lazy} keyword.
One can see examples of that technique in the source code of \Coq{},
for example
-\verb+tactics/contrib/polynom/ring.ml+ or
-\verb+tactics/contrib/polynom/coq_omega.ml+.
+\verb+plugins/omega/coq_omega.ml+.
\section[Some Useful Tools for Writing Tactics]{Some Useful Tools for Writing Tactics\label{SomeUsefulToolsforWrittingTactics}}
When the implementation of a tactic is not a straightforward
diff --git a/contrib/cc/README b/plugins/cc/README
index 073b140ea..073b140ea 100644
--- a/contrib/cc/README
+++ b/plugins/cc/README
diff --git a/contrib/cc/cc_plugin.mllib b/plugins/cc/cc_plugin.mllib
index 27e903fd3..27e903fd3 100644
--- a/contrib/cc/cc_plugin.mllib
+++ b/plugins/cc/cc_plugin.mllib
diff --git a/contrib/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 2d7dd9d6c..2d7dd9d6c 100644
--- a/contrib/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
diff --git a/contrib/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 3bd52b6e1..3bd52b6e1 100644
--- a/contrib/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
diff --git a/contrib/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 1e57aa6cb..1e57aa6cb 100644
--- a/contrib/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
diff --git a/contrib/cc/ccproof.mli b/plugins/cc/ccproof.mli
index 7fd28390f..7fd28390f 100644
--- a/contrib/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
diff --git a/contrib/cc/cctac.ml b/plugins/cc/cctac.ml
index 515d4aa93..515d4aa93 100644
--- a/contrib/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
diff --git a/contrib/cc/cctac.mli b/plugins/cc/cctac.mli
index 7cdd46ab4..7cdd46ab4 100644
--- a/contrib/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
diff --git a/contrib/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index f23ed49b6..f23ed49b6 100644
--- a/contrib/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
diff --git a/contrib/dp/Dp.v b/plugins/dp/Dp.v
index 47d67725f..47d67725f 100644
--- a/contrib/dp/Dp.v
+++ b/plugins/dp/Dp.v
diff --git a/contrib/dp/TODO b/plugins/dp/TODO
index 44349e214..44349e214 100644
--- a/contrib/dp/TODO
+++ b/plugins/dp/TODO
diff --git a/contrib/dp/dp.ml b/plugins/dp/dp.ml
index 79ffaf3f9..79ffaf3f9 100644
--- a/contrib/dp/dp.ml
+++ b/plugins/dp/dp.ml
diff --git a/contrib/dp/dp.mli b/plugins/dp/dp.mli
index 6dbc05e17..6dbc05e17 100644
--- a/contrib/dp/dp.mli
+++ b/plugins/dp/dp.mli
diff --git a/contrib/dp/dp_gappa.ml b/plugins/dp/dp_gappa.ml
index 9c035aa85..9c035aa85 100644
--- a/contrib/dp/dp_gappa.ml
+++ b/plugins/dp/dp_gappa.ml
diff --git a/contrib/dp/dp_plugin.mllib b/plugins/dp/dp_plugin.mllib
index 361d6f832..361d6f832 100644
--- a/contrib/dp/dp_plugin.mllib
+++ b/plugins/dp/dp_plugin.mllib
diff --git a/contrib/dp/dp_why.ml b/plugins/dp/dp_why.ml
index e24049ad6..e24049ad6 100644
--- a/contrib/dp/dp_why.ml
+++ b/plugins/dp/dp_why.ml
diff --git a/contrib/dp/dp_why.mli b/plugins/dp/dp_why.mli
index b38a3d376..b38a3d376 100644
--- a/contrib/dp/dp_why.mli
+++ b/plugins/dp/dp_why.mli
diff --git a/contrib/dp/dp_zenon.mli b/plugins/dp/dp_zenon.mli
index 0a727d1f1..0a727d1f1 100644
--- a/contrib/dp/dp_zenon.mli
+++ b/plugins/dp/dp_zenon.mli
diff --git a/contrib/dp/dp_zenon.mll b/plugins/dp/dp_zenon.mll
index e15e280db..e15e280db 100644
--- a/contrib/dp/dp_zenon.mll
+++ b/plugins/dp/dp_zenon.mll
diff --git a/contrib/dp/fol.mli b/plugins/dp/fol.mli
index b94bd3e35..b94bd3e35 100644
--- a/contrib/dp/fol.mli
+++ b/plugins/dp/fol.mli
diff --git a/contrib/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4
index 95135694d..95135694d 100644
--- a/contrib/dp/g_dp.ml4
+++ b/plugins/dp/g_dp.ml4
diff --git a/contrib/dp/test2.v b/plugins/dp/test2.v
index 3e4c0f6dd..3e4c0f6dd 100644
--- a/contrib/dp/test2.v
+++ b/plugins/dp/test2.v
diff --git a/contrib/dp/test_gappa.v b/plugins/dp/test_gappa.v
index eb65a59d6..eb65a59d6 100644
--- a/contrib/dp/test_gappa.v
+++ b/plugins/dp/test_gappa.v
diff --git a/contrib/dp/tests.v b/plugins/dp/tests.v
index a6d4f2e13..fa6a13ef0 100644
--- a/contrib/dp/tests.v
+++ b/plugins/dp/tests.v
@@ -160,7 +160,7 @@ simplify.
Qed.
-(* Inductive types definitions - call to incontrib/dp/jection function *)
+(* Inductive types definitions - call to dp/injection function *)
Inductive even : Z -> Prop :=
| even_0 : even 0
diff --git a/contrib/dp/zenon.v b/plugins/dp/zenon.v
index 502465c6b..502465c6b 100644
--- a/contrib/dp/zenon.v
+++ b/plugins/dp/zenon.v
diff --git a/contrib/extraction/CHANGES b/plugins/extraction/CHANGES
index 94531c47e..fbcd01a15 100644
--- a/contrib/extraction/CHANGES
+++ b/plugins/extraction/CHANGES
@@ -79,7 +79,7 @@ but also a few steps toward a more user-friendly extraction:
were one would have been enough.
- Examples of code needing those Obj.magic:
- * contrib/extraction/test_extraction.v in the Coq source
+ * plugins/extraction/test_extraction.v in the Coq source
* in the users' contributions:
Lannion
Lyon/CIRCUITS
diff --git a/contrib/extraction/README b/plugins/extraction/README
index 64c871fd3..64c871fd3 100644
--- a/contrib/extraction/README
+++ b/plugins/extraction/README
diff --git a/contrib/extraction/common.ml b/plugins/extraction/common.ml
index 11c3b3b5b..11c3b3b5b 100644
--- a/contrib/extraction/common.ml
+++ b/plugins/extraction/common.ml
diff --git a/contrib/extraction/common.mli b/plugins/extraction/common.mli
index c401bd059..c401bd059 100644
--- a/contrib/extraction/common.mli
+++ b/plugins/extraction/common.mli
diff --git a/contrib/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 39e277081..39e277081 100644
--- a/contrib/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
diff --git a/contrib/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index dcb4601e5..dcb4601e5 100644
--- a/contrib/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
diff --git a/contrib/extraction/extraction.ml b/plugins/extraction/extraction.ml
index ffaefd5e3..ffaefd5e3 100644
--- a/contrib/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
diff --git a/contrib/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 2c534ea7b..2c534ea7b 100644
--- a/contrib/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
diff --git a/contrib/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mllib
index bb87b9e32..bb87b9e32 100644
--- a/contrib/extraction/extraction_plugin.mllib
+++ b/plugins/extraction/extraction_plugin.mllib
diff --git a/contrib/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 2b561616b..2b561616b 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
diff --git a/contrib/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 6403e7bbe..6403e7bbe 100644
--- a/contrib/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
diff --git a/contrib/extraction/haskell.mli b/plugins/extraction/haskell.mli
index 1b5dbc711..1b5dbc711 100644
--- a/contrib/extraction/haskell.mli
+++ b/plugins/extraction/haskell.mli
diff --git a/contrib/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 12ca9ad75..12ca9ad75 100644
--- a/contrib/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
diff --git a/contrib/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 213df31e6..213df31e6 100644
--- a/contrib/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
diff --git a/contrib/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 4b6b47ab9..4b6b47ab9 100644
--- a/contrib/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
diff --git a/contrib/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 0394ea4b7..0394ea4b7 100644
--- a/contrib/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
diff --git a/contrib/extraction/modutil.mli b/plugins/extraction/modutil.mli
index 8e04a368e..8e04a368e 100644
--- a/contrib/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
diff --git a/contrib/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 93fc2c2dc..93fc2c2dc 100644
--- a/contrib/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
diff --git a/contrib/extraction/ocaml.mli b/plugins/extraction/ocaml.mli
index 4a1c1778f..4a1c1778f 100644
--- a/contrib/extraction/ocaml.mli
+++ b/plugins/extraction/ocaml.mli
diff --git a/contrib/extraction/scheme.ml b/plugins/extraction/scheme.ml
index eaa47f5f9..eaa47f5f9 100644
--- a/contrib/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
diff --git a/contrib/extraction/scheme.mli b/plugins/extraction/scheme.mli
index b0fa395c6..b0fa395c6 100644
--- a/contrib/extraction/scheme.mli
+++ b/plugins/extraction/scheme.mli
diff --git a/contrib/extraction/table.ml b/plugins/extraction/table.ml
index f1e8f42fe..f1e8f42fe 100644
--- a/contrib/extraction/table.ml
+++ b/plugins/extraction/table.ml
diff --git a/contrib/extraction/table.mli b/plugins/extraction/table.mli
index 6e3f2ec56..6e3f2ec56 100644
--- a/contrib/extraction/table.mli
+++ b/plugins/extraction/table.mli
diff --git a/contrib/field/LegacyField.v b/plugins/field/LegacyField.v
index efa53b4e9..efa53b4e9 100644
--- a/contrib/field/LegacyField.v
+++ b/plugins/field/LegacyField.v
diff --git a/contrib/field/LegacyField_Compl.v b/plugins/field/LegacyField_Compl.v
index 746e7c997..746e7c997 100644
--- a/contrib/field/LegacyField_Compl.v
+++ b/plugins/field/LegacyField_Compl.v
diff --git a/contrib/field/LegacyField_Tactic.v b/plugins/field/LegacyField_Tactic.v
index 63d9bdda6..63d9bdda6 100644
--- a/contrib/field/LegacyField_Tactic.v
+++ b/plugins/field/LegacyField_Tactic.v
diff --git a/contrib/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v
index 131ba84b8..131ba84b8 100644
--- a/contrib/field/LegacyField_Theory.v
+++ b/plugins/field/LegacyField_Theory.v
diff --git a/contrib/field/field.ml4 b/plugins/field/field.ml4
index 93de6118b..93de6118b 100644
--- a/contrib/field/field.ml4
+++ b/plugins/field/field.ml4
diff --git a/contrib/field/field_plugin.mllib b/plugins/field/field_plugin.mllib
index 63492a64f..63492a64f 100644
--- a/contrib/field/field_plugin.mllib
+++ b/plugins/field/field_plugin.mllib
diff --git a/contrib/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 0be3a4b39..0be3a4b39 100644
--- a/contrib/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
diff --git a/contrib/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 9e9d1e122..9e9d1e122 100644
--- a/contrib/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
diff --git a/contrib/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index d7c5b66ae..d7c5b66ae 100644
--- a/contrib/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
diff --git a/contrib/firstorder/ground.ml b/plugins/firstorder/ground.ml
index a8d5fc2ef..a8d5fc2ef 100644
--- a/contrib/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
diff --git a/contrib/firstorder/ground.mli b/plugins/firstorder/ground.mli
index 3c0e903fd..3c0e903fd 100644
--- a/contrib/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
diff --git a/contrib/firstorder/ground_plugin.mllib b/plugins/firstorder/ground_plugin.mllib
index 863ccb50e..863ccb50e 100644
--- a/contrib/firstorder/ground_plugin.mllib
+++ b/plugins/firstorder/ground_plugin.mllib
diff --git a/contrib/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 3e087cd8b..3e087cd8b 100644
--- a/contrib/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
diff --git a/contrib/firstorder/instances.mli b/plugins/firstorder/instances.mli
index aed2ec83d..aed2ec83d 100644
--- a/contrib/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
diff --git a/contrib/firstorder/rules.ml b/plugins/firstorder/rules.ml
index fc31ee6fc..fc31ee6fc 100644
--- a/contrib/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
diff --git a/contrib/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 1c2c93a49..1c2c93a49 100644
--- a/contrib/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
diff --git a/contrib/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index fd5972fb7..fd5972fb7 100644
--- a/contrib/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
diff --git a/contrib/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 51db9de16..51db9de16 100644
--- a/contrib/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
diff --git a/contrib/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 782129e5c..782129e5c 100644
--- a/contrib/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
diff --git a/contrib/firstorder/unify.mli b/plugins/firstorder/unify.mli
index d6cb3a082..d6cb3a082 100644
--- a/contrib/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
diff --git a/contrib/fourier/Fourier.v b/plugins/fourier/Fourier.v
index 07b2973a4..07b2973a4 100644
--- a/contrib/fourier/Fourier.v
+++ b/plugins/fourier/Fourier.v
diff --git a/contrib/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v
index c592af09a..c592af09a 100644
--- a/contrib/fourier/Fourier_util.v
+++ b/plugins/fourier/Fourier_util.v
diff --git a/contrib/fourier/fourier.ml b/plugins/fourier/fourier.ml
index dd54aea29..dd54aea29 100644
--- a/contrib/fourier/fourier.ml
+++ b/plugins/fourier/fourier.ml
diff --git a/contrib/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 908267700..908267700 100644
--- a/contrib/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
diff --git a/contrib/fourier/fourier_plugin.mllib b/plugins/fourier/fourier_plugin.mllib
index b6262f8ae..b6262f8ae 100644
--- a/contrib/fourier/fourier_plugin.mllib
+++ b/plugins/fourier/fourier_plugin.mllib
diff --git a/contrib/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index b952851fa..b952851fa 100644
--- a/contrib/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.ml4
diff --git a/contrib/funind/Recdef.v b/plugins/funind/Recdef.v
index 2d206220e..2d206220e 100644
--- a/contrib/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
diff --git a/contrib/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index adfb9ce2f..adfb9ce2f 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
diff --git a/contrib/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 62eb528e0..62eb528e0 100644
--- a/contrib/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
diff --git a/contrib/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 49d1a179b..49d1a179b 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
diff --git a/contrib/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index cf28c6e6c..cf28c6e6c 100644
--- a/contrib/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
diff --git a/contrib/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 28fec2e98..28fec2e98 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
diff --git a/contrib/funind/indfun.ml b/plugins/funind/indfun.ml
index 348a17b11..348a17b11 100644
--- a/contrib/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
diff --git a/contrib/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 69cc0607b..69cc0607b 100644
--- a/contrib/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
diff --git a/contrib/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index e9aa692b6..e9aa692b6 100644
--- a/contrib/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
diff --git a/contrib/funind/invfun.ml b/plugins/funind/invfun.ml
index 5f8587408..5f8587408 100644
--- a/contrib/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
diff --git a/contrib/funind/merge.ml b/plugins/funind/merge.ml
index 9bbd165df..092830025 100644
--- a/contrib/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -1028,7 +1028,7 @@ let relprinctype_to_funprinctype relprinctype nfuns =
*)
(*
*** Local Variables: ***
-*** compile-command: "make -C ../.. contrib/funind/merge.cmo" ***
+*** compile-command: "make -C ../.. plugins/funind/merge.cmo" ***
*** indent-tabs-mode: nil ***
*** End: ***
*)
diff --git a/contrib/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 7e9ba3f8e..7e9ba3f8e 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
diff --git a/contrib/funind/rawterm_to_relation.mli b/plugins/funind/rawterm_to_relation.mli
index 0075fb0a0..0075fb0a0 100644
--- a/contrib/funind/rawterm_to_relation.mli
+++ b/plugins/funind/rawterm_to_relation.mli
diff --git a/contrib/funind/rawtermops.ml b/plugins/funind/rawtermops.ml
index 92396af59..92396af59 100644
--- a/contrib/funind/rawtermops.ml
+++ b/plugins/funind/rawtermops.ml
diff --git a/contrib/funind/rawtermops.mli b/plugins/funind/rawtermops.mli
index 358c6ba6c..358c6ba6c 100644
--- a/contrib/funind/rawtermops.mli
+++ b/plugins/funind/rawtermops.mli
diff --git a/contrib/funind/recdef.ml b/plugins/funind/recdef.ml
index a96ec6a43..a96ec6a43 100644
--- a/contrib/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
diff --git a/contrib/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mllib
index c30ee212f..c30ee212f 100644
--- a/contrib/funind/recdef_plugin.mllib
+++ b/plugins/funind/recdef_plugin.mllib
diff --git a/contrib/groebner/GroebnerR.v b/plugins/groebner/GroebnerR.v
index 71e244126..71e244126 100644
--- a/contrib/groebner/GroebnerR.v
+++ b/plugins/groebner/GroebnerR.v
diff --git a/contrib/groebner/GroebnerZ.v b/plugins/groebner/GroebnerZ.v
index da79a36f7..da79a36f7 100644
--- a/contrib/groebner/GroebnerZ.v
+++ b/plugins/groebner/GroebnerZ.v
diff --git a/contrib/groebner/groebner.ml4 b/plugins/groebner/groebner.ml4
index 00cd8ae5d..00cd8ae5d 100644
--- a/contrib/groebner/groebner.ml4
+++ b/plugins/groebner/groebner.ml4
diff --git a/contrib/groebner/groebner_plugin.mllib b/plugins/groebner/groebner_plugin.mllib
index 1da12fcf2..1da12fcf2 100644
--- a/contrib/groebner/groebner_plugin.mllib
+++ b/plugins/groebner/groebner_plugin.mllib
diff --git a/contrib/groebner/ideal.ml b/plugins/groebner/ideal.ml
index a87a9972b..a87a9972b 100644
--- a/contrib/groebner/ideal.ml
+++ b/plugins/groebner/ideal.ml
diff --git a/contrib/groebner/ideal.mli b/plugins/groebner/ideal.mli
index 48b81102e..48b81102e 100644
--- a/contrib/groebner/ideal.mli
+++ b/plugins/groebner/ideal.mli
diff --git a/contrib/groebner/polynom.ml b/plugins/groebner/polynom.ml
index 5c859f755..5c859f755 100644
--- a/contrib/groebner/polynom.ml
+++ b/plugins/groebner/polynom.ml
diff --git a/contrib/groebner/polynom.mli b/plugins/groebner/polynom.mli
index 99c1701b8..99c1701b8 100644
--- a/contrib/groebner/polynom.mli
+++ b/plugins/groebner/polynom.mli
diff --git a/contrib/groebner/utile.ml b/plugins/groebner/utile.ml
index 52a69dc10..52a69dc10 100644
--- a/contrib/groebner/utile.ml
+++ b/plugins/groebner/utile.ml
diff --git a/contrib/groebner/utile.mli b/plugins/groebner/utile.mli
index 209258dd6..209258dd6 100644
--- a/contrib/groebner/utile.mli
+++ b/plugins/groebner/utile.mli
diff --git a/contrib/interface/COPYRIGHT b/plugins/interface/COPYRIGHT
index 23aeb6bb2..824838309 100644
--- a/contrib/interface/COPYRIGHT
+++ b/plugins/interface/COPYRIGHT
@@ -7,7 +7,7 @@
(* *)
(*****************************************************************************)
-The current directory contrib/interface implements Coq support for the
+The current directory plugins/interface implements Coq support for the
Pcoq Graphical Interface of Coq. It has been developed by Yves Bertot
with contributions from Loïc Pottier and Laurence Rideau.
diff --git a/contrib/interface/CoqInterface.v b/plugins/interface/CoqInterface.v
index e86fb2fce..e86fb2fce 100644
--- a/contrib/interface/CoqInterface.v
+++ b/plugins/interface/CoqInterface.v
diff --git a/contrib/interface/CoqParser.v b/plugins/interface/CoqParser.v
index db4aa06dc..db4aa06dc 100644
--- a/contrib/interface/CoqParser.v
+++ b/plugins/interface/CoqParser.v
diff --git a/contrib/interface/ascent.mli b/plugins/interface/ascent.mli
index f0b68fb7c..f0b68fb7c 100644
--- a/contrib/interface/ascent.mli
+++ b/plugins/interface/ascent.mli
diff --git a/contrib/interface/blast.ml b/plugins/interface/blast.ml
index 57b4d1af8..57b4d1af8 100644
--- a/contrib/interface/blast.ml
+++ b/plugins/interface/blast.ml
diff --git a/contrib/interface/blast.mli b/plugins/interface/blast.mli
index f67019439..f67019439 100644
--- a/contrib/interface/blast.mli
+++ b/plugins/interface/blast.mli
diff --git a/contrib/interface/centaur.ml4 b/plugins/interface/centaur.ml4
index f8c088779..f8c088779 100644
--- a/contrib/interface/centaur.ml4
+++ b/plugins/interface/centaur.ml4
diff --git a/contrib/interface/coqinterface_plugin.mllib b/plugins/interface/coqinterface_plugin.mllib
index e4b575b13..e4b575b13 100644
--- a/contrib/interface/coqinterface_plugin.mllib
+++ b/plugins/interface/coqinterface_plugin.mllib
diff --git a/contrib/interface/coqparser.ml b/plugins/interface/coqparser.ml
index 5de6060f0..a63e18d27 100644
--- a/contrib/interface/coqparser.ml
+++ b/plugins/interface/coqparser.ml
@@ -378,7 +378,7 @@ Libobject.relax true;
begin
add_rec_path (Filename.concat coqdir "theories")
(Names.make_dirpath [Nameops.coq_root]);
- add_rec_path (Filename.concat coqdir "contrib")
+ add_rec_path (Filename.concat coqdir "plugins")
(Names.make_dirpath [Nameops.coq_root])
end;
(let vernacrc =
@@ -388,7 +388,7 @@ Libobject.relax true;
Not_found ->
List.fold_left
(fun s1 s2 -> (Filename.concat s1 s2))
- coqdir [ "contrib"; "interface"; "vernacrc"] in
+ coqdir [ "plugins"; "interface"; "vernacrc"] in
try
(Gramext.warning_verbose := false;
coqparser_loop (open_in vernacrc))
diff --git a/contrib/interface/coqparser_plugin.mllib b/plugins/interface/coqparser_plugin.mllib
index 65ec57715..65ec57715 100644
--- a/contrib/interface/coqparser_plugin.mllib
+++ b/plugins/interface/coqparser_plugin.mllib
diff --git a/contrib/interface/dad.ml b/plugins/interface/dad.ml
index c2ab2dc8d..c2ab2dc8d 100644
--- a/contrib/interface/dad.ml
+++ b/plugins/interface/dad.ml
diff --git a/contrib/interface/dad.mli b/plugins/interface/dad.mli
index f556c1926..f556c1926 100644
--- a/contrib/interface/dad.mli
+++ b/plugins/interface/dad.mli
diff --git a/contrib/interface/debug_tac.ml4 b/plugins/interface/debug_tac.ml4
index aad3a765d..aad3a765d 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/plugins/interface/debug_tac.ml4
diff --git a/contrib/interface/debug_tac.mli b/plugins/interface/debug_tac.mli
index da4bbaa09..da4bbaa09 100644
--- a/contrib/interface/debug_tac.mli
+++ b/plugins/interface/debug_tac.mli
diff --git a/contrib/interface/depends.ml b/plugins/interface/depends.ml
index e59de34a4..e59de34a4 100644
--- a/contrib/interface/depends.ml
+++ b/plugins/interface/depends.ml
diff --git a/contrib/interface/history.ml b/plugins/interface/history.ml
index f73c20849..f73c20849 100644
--- a/contrib/interface/history.ml
+++ b/plugins/interface/history.ml
diff --git a/contrib/interface/history.mli b/plugins/interface/history.mli
index 053883f0d..053883f0d 100644
--- a/contrib/interface/history.mli
+++ b/plugins/interface/history.mli
diff --git a/contrib/interface/line_parser.ml4 b/plugins/interface/line_parser.ml4
index 0b13a092a..0b13a092a 100755
--- a/contrib/interface/line_parser.ml4
+++ b/plugins/interface/line_parser.ml4
diff --git a/contrib/interface/line_parser.mli b/plugins/interface/line_parser.mli
index b0b043c75..b0b043c75 100644
--- a/contrib/interface/line_parser.mli
+++ b/plugins/interface/line_parser.mli
diff --git a/contrib/interface/name_to_ast.ml b/plugins/interface/name_to_ast.ml
index 668a581e1..668a581e1 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/plugins/interface/name_to_ast.ml
diff --git a/contrib/interface/name_to_ast.mli b/plugins/interface/name_to_ast.mli
index f9e83b5e1..f9e83b5e1 100644
--- a/contrib/interface/name_to_ast.mli
+++ b/plugins/interface/name_to_ast.mli
diff --git a/contrib/interface/paths.ml b/plugins/interface/paths.ml
index a157ca925..a157ca925 100644
--- a/contrib/interface/paths.ml
+++ b/plugins/interface/paths.ml
diff --git a/contrib/interface/paths.mli b/plugins/interface/paths.mli
index 266207238..266207238 100644
--- a/contrib/interface/paths.mli
+++ b/plugins/interface/paths.mli
diff --git a/contrib/interface/pbp.ml b/plugins/interface/pbp.ml
index 01747aa58..01747aa58 100644
--- a/contrib/interface/pbp.ml
+++ b/plugins/interface/pbp.ml
diff --git a/contrib/interface/pbp.mli b/plugins/interface/pbp.mli
index 9daba1844..9daba1844 100644
--- a/contrib/interface/pbp.mli
+++ b/plugins/interface/pbp.mli
diff --git a/contrib/interface/showproof.ml b/plugins/interface/showproof.ml
index 2ab62763d..2ab62763d 100644
--- a/contrib/interface/showproof.ml
+++ b/plugins/interface/showproof.ml
diff --git a/contrib/interface/showproof.mli b/plugins/interface/showproof.mli
index 9b6787b7c..9b6787b7c 100755
--- a/contrib/interface/showproof.mli
+++ b/plugins/interface/showproof.mli
diff --git a/contrib/interface/showproof_ct.ml b/plugins/interface/showproof_ct.ml
index dd7f455d7..dd7f455d7 100644
--- a/contrib/interface/showproof_ct.ml
+++ b/plugins/interface/showproof_ct.ml
diff --git a/contrib/interface/translate.ml b/plugins/interface/translate.ml
index 559860b2f..559860b2f 100644
--- a/contrib/interface/translate.ml
+++ b/plugins/interface/translate.ml
diff --git a/contrib/interface/translate.mli b/plugins/interface/translate.mli
index 34841fc4b..34841fc4b 100644
--- a/contrib/interface/translate.mli
+++ b/plugins/interface/translate.mli
diff --git a/contrib/interface/vernacrc b/plugins/interface/vernacrc
index 14f7e8c98..14f7e8c98 100644
--- a/contrib/interface/vernacrc
+++ b/plugins/interface/vernacrc
diff --git a/contrib/interface/vtp.ml b/plugins/interface/vtp.ml
index 1714440df..1714440df 100644
--- a/contrib/interface/vtp.ml
+++ b/plugins/interface/vtp.ml
diff --git a/contrib/interface/vtp.mli b/plugins/interface/vtp.mli
index d7bd8db53..d7bd8db53 100644
--- a/contrib/interface/vtp.mli
+++ b/plugins/interface/vtp.mli
diff --git a/contrib/interface/xlate.ml b/plugins/interface/xlate.ml
index 64a9b5c8c..64a9b5c8c 100644
--- a/contrib/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
diff --git a/contrib/interface/xlate.mli b/plugins/interface/xlate.mli
index 2e2b95fe7..2e2b95fe7 100644
--- a/contrib/interface/xlate.mli
+++ b/plugins/interface/xlate.mli
diff --git a/contrib/micromega/CheckerMaker.v b/plugins/micromega/CheckerMaker.v
index 93b4d213f..93b4d213f 100644
--- a/contrib/micromega/CheckerMaker.v
+++ b/plugins/micromega/CheckerMaker.v
diff --git a/contrib/micromega/Env.v b/plugins/micromega/Env.v
index 40db9e464..631417e0e 100644
--- a/contrib/micromega/Env.v
+++ b/plugins/micromega/Env.v
@@ -17,7 +17,7 @@ Require Import Coq.Arith.Max.
Require Import List.
Set Implicit Arguments.
-(* I have addded a Leaf constructor to the varmap data structure (/contrib/ring/Quote.v)
+(* I have addded a Leaf constructor to the varmap data structure (/plugins/ring/Quote.v)
-- this is harmless and spares a lot of Empty.
This means smaller proof-terms.
BTW, by dropping the polymorphism, I get small (yet noticeable) speed-up.
diff --git a/contrib/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 04e68272e..04e68272e 100644
--- a/contrib/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
diff --git a/contrib/micromega/LICENSE.sos b/plugins/micromega/LICENSE.sos
index 5aadfa2a6..5aadfa2a6 100644
--- a/contrib/micromega/LICENSE.sos
+++ b/plugins/micromega/LICENSE.sos
diff --git a/contrib/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index a5ac92db8..a5ac92db8 100644
--- a/contrib/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
diff --git a/contrib/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v
index 149b77316..149b77316 100644
--- a/contrib/micromega/OrderedRing.v
+++ b/plugins/micromega/OrderedRing.v
diff --git a/contrib/micromega/Psatz.v b/plugins/micromega/Psatz.v
index a3be56207..a3be56207 100644
--- a/contrib/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
diff --git a/contrib/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index f02209459..f02209459 100644
--- a/contrib/micromega/QMicromega.v
+++ b/plugins/micromega/QMicromega.v
diff --git a/contrib/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 70786a057..70786a057 100644
--- a/contrib/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
diff --git a/contrib/micromega/Refl.v b/plugins/micromega/Refl.v
index 801d8b212..801d8b212 100644
--- a/contrib/micromega/Refl.v
+++ b/plugins/micromega/Refl.v
diff --git a/contrib/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 6885b82cd..6885b82cd 100644
--- a/contrib/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
diff --git a/contrib/micromega/Tauto.v b/plugins/micromega/Tauto.v
index ef48efa6d..ef48efa6d 100644
--- a/contrib/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
diff --git a/contrib/micromega/VarMap.v b/plugins/micromega/VarMap.v
index 240c0fb7c..ed204d92b 100644
--- a/contrib/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -17,7 +17,7 @@ Require Import Coq.Arith.Max.
Require Import List.
Set Implicit Arguments.
-(* I have addded a Leaf constructor to the varmap data structure (/contrib/ring/Quote.v)
+(* I have addded a Leaf constructor to the varmap data structure (/plugins/ring/Quote.v)
-- this is harmless and spares a lot of Empty.
This means smaller proof-terms.
BTW, by dropping the polymorphism, I get small (yet noticeable) speed-up.
@@ -43,7 +43,7 @@ Section MakeVarMap.
end
end.
- (* an off_map (a map with offset) offers the same functionalites as /contrib/setoid_ring/BinList.v - it is used in EnvRing.v *)
+ (* an off_map (a map with offset) offers the same functionalites as /plugins/setoid_ring/BinList.v - it is used in EnvRing.v *)
(*
Definition off_map := (option positive *t )%type.
diff --git a/contrib/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index ced67e39d..ced67e39d 100644
--- a/contrib/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
diff --git a/contrib/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 1da3228a9..1da3228a9 100644
--- a/contrib/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
diff --git a/contrib/micromega/certificate.ml b/plugins/micromega/certificate.ml
index a297c1633..a297c1633 100644
--- a/contrib/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
diff --git a/contrib/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index e9a8a0e3b..3e88af9f0 100644
--- a/contrib/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1295,7 +1295,7 @@ let call_csdpcert provername poly =
close_out ch_to;
let cmdname =
List.fold_left Filename.concat (Envars.coqlib ())
- ["contrib"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in
+ ["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in
let c = Sys.command (cmdname ^" "^ tmp_to ^" "^ tmp_from) in
(try Sys.remove tmp_to with _ -> ());
if c <> 0 then Util.error ("Failed to call csdp certificate generator");
diff --git a/contrib/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index e451a38fd..e451a38fd 100644
--- a/contrib/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
diff --git a/contrib/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 23ae3bd0e..23ae3bd0e 100644
--- a/contrib/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
diff --git a/contrib/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index c2eb572c9..c2eb572c9 100644
--- a/contrib/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
diff --git a/contrib/micromega/micromega.ml b/plugins/micromega/micromega.ml
index e151e4e1d..e151e4e1d 100644
--- a/contrib/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
diff --git a/contrib/micromega/micromega.mli b/plugins/micromega/micromega.mli
index f94f091e8..f94f091e8 100644
--- a/contrib/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
diff --git a/contrib/micromega/micromega_plugin.mllib b/plugins/micromega/micromega_plugin.mllib
index 41753542f..41753542f 100644
--- a/contrib/micromega/micromega_plugin.mllib
+++ b/plugins/micromega/micromega_plugin.mllib
diff --git a/contrib/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 03e3999fd..03e3999fd 100644
--- a/contrib/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
diff --git a/contrib/micromega/sos.ml b/plugins/micromega/sos.ml
index e3d72ed9a..e3d72ed9a 100644
--- a/contrib/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
diff --git a/contrib/micromega/sos.mli b/plugins/micromega/sos.mli
index 31c9518c8..31c9518c8 100644
--- a/contrib/micromega/sos.mli
+++ b/plugins/micromega/sos.mli
diff --git a/contrib/omega/Omega.v b/plugins/omega/Omega.v
index 30b945718..30b945718 100644
--- a/contrib/omega/Omega.v
+++ b/plugins/omega/Omega.v
diff --git a/contrib/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v
index fe8fcc924..fe8fcc924 100644
--- a/contrib/omega/OmegaLemmas.v
+++ b/plugins/omega/OmegaLemmas.v
diff --git a/contrib/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v
index 21535f0d3..21535f0d3 100644
--- a/contrib/omega/OmegaPlugin.v
+++ b/plugins/omega/OmegaPlugin.v
diff --git a/contrib/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 47e22a97f..47e22a97f 100644
--- a/contrib/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
diff --git a/contrib/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 535459885..535459885 100644
--- a/contrib/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
diff --git a/contrib/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index a69f8ef74..a69f8ef74 100644
--- a/contrib/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
diff --git a/contrib/omega/omega.ml b/plugins/omega/omega.ml
index fd774c16d..fd774c16d 100644
--- a/contrib/omega/omega.ml
+++ b/plugins/omega/omega.ml
diff --git a/contrib/omega/omega_plugin.mllib b/plugins/omega/omega_plugin.mllib
index 020901376..020901376 100644
--- a/contrib/omega/omega_plugin.mllib
+++ b/plugins/omega/omega_plugin.mllib
diff --git a/contrib/quote/Quote.v b/plugins/quote/Quote.v
index f21a678e1..f21a678e1 100644
--- a/contrib/quote/Quote.v
+++ b/plugins/quote/Quote.v
diff --git a/contrib/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 808cbbf27..808cbbf27 100644
--- a/contrib/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
diff --git a/contrib/quote/quote.ml b/plugins/quote/quote.ml
index 9141dc2f5..9141dc2f5 100644
--- a/contrib/quote/quote.ml
+++ b/plugins/quote/quote.ml
diff --git a/contrib/quote/quote_plugin.mllib b/plugins/quote/quote_plugin.mllib
index 21810acdf..21810acdf 100644
--- a/contrib/quote/quote_plugin.mllib
+++ b/plugins/quote/quote_plugin.mllib
diff --git a/contrib/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v
index 959d66c74..959d66c74 100644
--- a/contrib/ring/LegacyArithRing.v
+++ b/plugins/ring/LegacyArithRing.v
diff --git a/contrib/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v
index ee9fb3761..ee9fb3761 100644
--- a/contrib/ring/LegacyNArithRing.v
+++ b/plugins/ring/LegacyNArithRing.v
diff --git a/contrib/ring/LegacyRing.v b/plugins/ring/LegacyRing.v
index 4ae85baf3..4ae85baf3 100644
--- a/contrib/ring/LegacyRing.v
+++ b/plugins/ring/LegacyRing.v
diff --git a/contrib/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v
index 79f6976bd..79f6976bd 100644
--- a/contrib/ring/LegacyRing_theory.v
+++ b/plugins/ring/LegacyRing_theory.v
diff --git a/contrib/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v
index 68a0dd275..68a0dd275 100644
--- a/contrib/ring/LegacyZArithRing.v
+++ b/plugins/ring/LegacyZArithRing.v
diff --git a/contrib/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v
index 9b85fb85e..9b85fb85e 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/plugins/ring/Ring_abstract.v
diff --git a/contrib/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v
index ad1cc5cf1..ad1cc5cf1 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/plugins/ring/Ring_normalize.v
diff --git a/contrib/ring/Setoid_ring.v b/plugins/ring/Setoid_ring.v
index 93b9bc7cf..93b9bc7cf 100644
--- a/contrib/ring/Setoid_ring.v
+++ b/plugins/ring/Setoid_ring.v
diff --git a/contrib/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v
index ce23d05af..ce23d05af 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/plugins/ring/Setoid_ring_normalize.v
diff --git a/contrib/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v
index f50a2f30a..f50a2f30a 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/plugins/ring/Setoid_ring_theory.v
diff --git a/contrib/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4
index 5ca1bfced..5ca1bfced 100644
--- a/contrib/ring/g_ring.ml4
+++ b/plugins/ring/g_ring.ml4
diff --git a/contrib/ring/ring.ml b/plugins/ring/ring.ml
index adcf51fe8..adcf51fe8 100644
--- a/contrib/ring/ring.ml
+++ b/plugins/ring/ring.ml
diff --git a/contrib/ring/ring_plugin.mllib b/plugins/ring/ring_plugin.mllib
index 183884ca6..183884ca6 100644
--- a/contrib/ring/ring_plugin.mllib
+++ b/plugins/ring/ring_plugin.mllib
diff --git a/contrib/romega/README b/plugins/romega/README
index 86c9e58af..86c9e58af 100644
--- a/contrib/romega/README
+++ b/plugins/romega/README
diff --git a/contrib/romega/ROmega.v b/plugins/romega/ROmega.v
index 3ddb6bed1..3ddb6bed1 100644
--- a/contrib/romega/ROmega.v
+++ b/plugins/romega/ROmega.v
diff --git a/contrib/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 12176d661..12176d661 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
diff --git a/contrib/romega/const_omega.ml b/plugins/romega/const_omega.ml
index bdec6bf45..bdec6bf45 100644
--- a/contrib/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
diff --git a/contrib/romega/const_omega.mli b/plugins/romega/const_omega.mli
index 0f00e9184..0f00e9184 100644
--- a/contrib/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
diff --git a/contrib/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 39b6c2106..39b6c2106 100644
--- a/contrib/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
diff --git a/contrib/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index fc4f7a8f0..fc4f7a8f0 100644
--- a/contrib/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
diff --git a/contrib/romega/romega_plugin.mllib b/plugins/romega/romega_plugin.mllib
index 38d0e9411..38d0e9411 100644
--- a/contrib/romega/romega_plugin.mllib
+++ b/plugins/romega/romega_plugin.mllib
diff --git a/contrib/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index cd0f1afe9..cd0f1afe9 100644
--- a/contrib/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
diff --git a/contrib/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v
index 4b95097e2..4b95097e2 100644
--- a/contrib/rtauto/Rtauto.v
+++ b/plugins/rtauto/Rtauto.v
diff --git a/contrib/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index 4cbe84368..4cbe84368 100644
--- a/contrib/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
diff --git a/contrib/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 9d9d66bb2..9d9d66bb2 100644
--- a/contrib/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
diff --git a/contrib/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli
index a0e86b8d6..a0e86b8d6 100644
--- a/contrib/rtauto/proof_search.mli
+++ b/plugins/rtauto/proof_search.mli
diff --git a/contrib/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 6cde1ddcf..6cde1ddcf 100644
--- a/contrib/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
diff --git a/contrib/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index a6d68a226..a6d68a226 100644
--- a/contrib/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
diff --git a/contrib/rtauto/rtauto_plugin.mllib b/plugins/rtauto/rtauto_plugin.mllib
index 61c5e945b..61c5e945b 100644
--- a/contrib/rtauto/rtauto_plugin.mllib
+++ b/plugins/rtauto/rtauto_plugin.mllib
diff --git a/contrib/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v
index 601cabe00..601cabe00 100644
--- a/contrib/setoid_ring/ArithRing.v
+++ b/plugins/setoid_ring/ArithRing.v
diff --git a/contrib/setoid_ring/BinList.v b/plugins/setoid_ring/BinList.v
index 509020042..509020042 100644
--- a/contrib/setoid_ring/BinList.v
+++ b/plugins/setoid_ring/BinList.v
diff --git a/contrib/setoid_ring/Field.v b/plugins/setoid_ring/Field.v
index a944ba5f0..a944ba5f0 100644
--- a/contrib/setoid_ring/Field.v
+++ b/plugins/setoid_ring/Field.v
diff --git a/contrib/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
index b31ebda55..b31ebda55 100644
--- a/contrib/setoid_ring/Field_tac.v
+++ b/plugins/setoid_ring/Field_tac.v
diff --git a/contrib/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index fd99f786f..fd99f786f 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
diff --git a/contrib/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index e664b3b76..e664b3b76 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
diff --git a/contrib/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v
index 0ba519fde..0ba519fde 100644
--- a/contrib/setoid_ring/NArithRing.v
+++ b/plugins/setoid_ring/NArithRing.v
diff --git a/contrib/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v
index 60641bcf9..60641bcf9 100644
--- a/contrib/setoid_ring/RealField.v
+++ b/plugins/setoid_ring/RealField.v
diff --git a/contrib/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v
index d01b16258..d01b16258 100644
--- a/contrib/setoid_ring/Ring.v
+++ b/plugins/setoid_ring/Ring.v
diff --git a/contrib/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v
index fd9dd8d0d..fd9dd8d0d 100644
--- a/contrib/setoid_ring/Ring_base.v
+++ b/plugins/setoid_ring/Ring_base.v
diff --git a/contrib/setoid_ring/Ring_equiv.v b/plugins/setoid_ring/Ring_equiv.v
index 945f6c684..945f6c684 100644
--- a/contrib/setoid_ring/Ring_equiv.v
+++ b/plugins/setoid_ring/Ring_equiv.v
diff --git a/contrib/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index d88470369..d88470369 100644
--- a/contrib/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
diff --git a/contrib/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v
index 44e97bda7..44e97bda7 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/plugins/setoid_ring/Ring_tac.v
diff --git a/contrib/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 531ab3ca5..531ab3ca5 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
diff --git a/contrib/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v
index 942915abf..942915abf 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/plugins/setoid_ring/ZArithRing.v
diff --git a/contrib/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 095e86133..926ac48d1 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -245,29 +245,29 @@ let rec dest_rel t =
(****************************************************************************)
(* Library linking *)
-let contrib_name = "setoid_ring"
+let plugin_dir = "setoid_ring"
-let cdir = ["Coq";contrib_name]
-let contrib_modules =
+let cdir = ["Coq";plugin_dir]
+let plugin_modules =
List.map (fun d -> cdir@d)
[["Ring_theory"];["Ring_polynom"]; ["Ring_tac"];["InitialRing"];
["Field_tac"]; ["Field_theory"]
]
let my_constant c =
- lazy (Coqlib.gen_constant_in_modules "Ring" contrib_modules c)
+ lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c)
let new_ring_path =
- make_dirpath (List.map id_of_string ["Ring_tac";contrib_name;"Coq"])
+ make_dirpath (List.map id_of_string ["Ring_tac";plugin_dir;"Coq"])
let ltac s =
lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s))
let znew_ring_path =
- make_dirpath (List.map id_of_string ["InitialRing";contrib_name;"Coq"])
+ make_dirpath (List.map id_of_string ["InitialRing";plugin_dir;"Coq"])
let zltac s =
lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s))
let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);;
-let pol_cst s = mk_cst [contrib_name;"Ring_polynom"] s ;;
+let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
(* Ring theory *)
@@ -851,7 +851,7 @@ END
(***********************************************************************)
let new_field_path =
- make_dirpath (List.map id_of_string ["Field_tac";contrib_name;"Coq"])
+ make_dirpath (List.map id_of_string ["Field_tac";plugin_dir;"Coq"])
let field_ltac s =
lazy(make_kn (MPfile new_field_path) (make_dirpath []) (mk_label s))
diff --git a/contrib/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib
index 54b7c8e67..54b7c8e67 100644
--- a/contrib/setoid_ring/newring_plugin.mllib
+++ b/plugins/setoid_ring/newring_plugin.mllib
diff --git a/contrib/subtac/equations.ml4 b/plugins/subtac/equations.ml4
index 5b76c9587..5b76c9587 100644
--- a/contrib/subtac/equations.ml4
+++ b/plugins/subtac/equations.ml4
diff --git a/contrib/subtac/eterm.ml b/plugins/subtac/eterm.ml
index 00a69bba7..00a69bba7 100644
--- a/contrib/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
diff --git a/contrib/subtac/eterm.mli b/plugins/subtac/eterm.mli
index 413823ffe..413823ffe 100644
--- a/contrib/subtac/eterm.mli
+++ b/plugins/subtac/eterm.mli
diff --git a/contrib/subtac/g_eterm.ml4 b/plugins/subtac/g_eterm.ml4
index 095e5fafc..095e5fafc 100644
--- a/contrib/subtac/g_eterm.ml4
+++ b/plugins/subtac/g_eterm.ml4
diff --git a/contrib/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index c1e168da1..c1e168da1 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
diff --git a/contrib/subtac/subtac.ml b/plugins/subtac/subtac.ml
index d10c8f68c..d10c8f68c 100644
--- a/contrib/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
diff --git a/contrib/subtac/subtac.mli b/plugins/subtac/subtac.mli
index b51150aa0..b51150aa0 100644
--- a/contrib/subtac/subtac.mli
+++ b/plugins/subtac/subtac.mli
diff --git a/contrib/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 00ed62ac8..00ed62ac8 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
diff --git a/contrib/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli
index 90989d2d3..90989d2d3 100644
--- a/contrib/subtac/subtac_cases.mli
+++ b/plugins/subtac/subtac_cases.mli
diff --git a/contrib/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 8ef215346..8ef215346 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
diff --git a/contrib/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli
index 917ed8059..917ed8059 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/plugins/subtac/subtac_classes.mli
diff --git a/contrib/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 54114b0b0..54114b0b0 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
diff --git a/contrib/subtac/subtac_coercion.mli b/plugins/subtac/subtac_coercion.mli
index 5678c10e6..5678c10e6 100644
--- a/contrib/subtac/subtac_coercion.mli
+++ b/plugins/subtac/subtac_coercion.mli
diff --git a/contrib/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 674805962..674805962 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
diff --git a/contrib/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
index 3a6a351ba..3a6a351ba 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/plugins/subtac/subtac_command.mli
diff --git a/contrib/subtac/subtac_errors.ml b/plugins/subtac/subtac_errors.ml
index 3bbfe22bc..3bbfe22bc 100644
--- a/contrib/subtac/subtac_errors.ml
+++ b/plugins/subtac/subtac_errors.ml
diff --git a/contrib/subtac/subtac_errors.mli b/plugins/subtac/subtac_errors.mli
index 8d75b9c01..8d75b9c01 100644
--- a/contrib/subtac/subtac_errors.mli
+++ b/plugins/subtac/subtac_errors.mli
diff --git a/contrib/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 8b8bb9ab4..8b8bb9ab4 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
diff --git a/contrib/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 60c0a4139..60c0a4139 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
diff --git a/contrib/subtac/subtac_plugin.mllib b/plugins/subtac/subtac_plugin.mllib
index 81b9ee2ba..81b9ee2ba 100644
--- a/contrib/subtac/subtac_plugin.mllib
+++ b/plugins/subtac/subtac_plugin.mllib
diff --git a/contrib/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index d9df5b34c..d9df5b34c 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
diff --git a/contrib/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli
index 1d8eb2507..1d8eb2507 100644
--- a/contrib/subtac/subtac_pretyping.mli
+++ b/plugins/subtac/subtac_pretyping.mli
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 01fe4ef6f..01fe4ef6f 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
diff --git a/contrib/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index ba30ee190..ba30ee190 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
diff --git a/contrib/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index 964f668f2..964f668f2 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
diff --git a/contrib/subtac/test/ListDep.v b/plugins/subtac/test/ListDep.v
index da612c436..da612c436 100644
--- a/contrib/subtac/test/ListDep.v
+++ b/plugins/subtac/test/ListDep.v
diff --git a/contrib/subtac/test/ListsTest.v b/plugins/subtac/test/ListsTest.v
index 05fc0803f..05fc0803f 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/plugins/subtac/test/ListsTest.v
diff --git a/contrib/subtac/test/Mutind.v b/plugins/subtac/test/Mutind.v
index ac49ca96a..ac49ca96a 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/plugins/subtac/test/Mutind.v
diff --git a/contrib/subtac/test/Test1.v b/plugins/subtac/test/Test1.v
index 14b808549..14b808549 100644
--- a/contrib/subtac/test/Test1.v
+++ b/plugins/subtac/test/Test1.v
diff --git a/contrib/subtac/test/euclid.v b/plugins/subtac/test/euclid.v
index 501aa7981..501aa7981 100644
--- a/contrib/subtac/test/euclid.v
+++ b/plugins/subtac/test/euclid.v
diff --git a/contrib/subtac/test/id.v b/plugins/subtac/test/id.v
index 9ae110881..9ae110881 100644
--- a/contrib/subtac/test/id.v
+++ b/plugins/subtac/test/id.v
diff --git a/contrib/subtac/test/measure.v b/plugins/subtac/test/measure.v
index 4f938f4f8..4f938f4f8 100644
--- a/contrib/subtac/test/measure.v
+++ b/plugins/subtac/test/measure.v
diff --git a/contrib/subtac/test/rec.v b/plugins/subtac/test/rec.v
index aaefd8cc5..aaefd8cc5 100644
--- a/contrib/subtac/test/rec.v
+++ b/plugins/subtac/test/rec.v
diff --git a/contrib/subtac/test/take.v b/plugins/subtac/test/take.v
index 2e17959c3..2e17959c3 100644
--- a/contrib/subtac/test/take.v
+++ b/plugins/subtac/test/take.v
diff --git a/contrib/subtac/test/wf.v b/plugins/subtac/test/wf.v
index 49fec2b80..49fec2b80 100644
--- a/contrib/subtac/test/wf.v
+++ b/plugins/subtac/test/wf.v
diff --git a/contrib/xml/COPYRIGHT b/plugins/xml/COPYRIGHT
index c8d231fd3..c8d231fd3 100644
--- a/contrib/xml/COPYRIGHT
+++ b/plugins/xml/COPYRIGHT
diff --git a/contrib/xml/README b/plugins/xml/README
index a45dd31a5..a45dd31a5 100644
--- a/contrib/xml/README
+++ b/plugins/xml/README
diff --git a/contrib/xml/acic.ml b/plugins/xml/acic.ml
index 032ddbebe..032ddbebe 100644
--- a/contrib/xml/acic.ml
+++ b/plugins/xml/acic.ml
diff --git a/contrib/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
index 64dc8a050..64dc8a050 100644
--- a/contrib/xml/acic2Xml.ml4
+++ b/plugins/xml/acic2Xml.ml4
diff --git a/contrib/xml/cic.dtd b/plugins/xml/cic.dtd
index c8035cab9..c8035cab9 100644
--- a/contrib/xml/cic.dtd
+++ b/plugins/xml/cic.dtd
diff --git a/contrib/xml/cic2Xml.ml b/plugins/xml/cic2Xml.ml
index 08d3a8501..08d3a8501 100644
--- a/contrib/xml/cic2Xml.ml
+++ b/plugins/xml/cic2Xml.ml
diff --git a/contrib/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 13e5e6d5f..13e5e6d5f 100644
--- a/contrib/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
diff --git a/contrib/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index 17d1d5dab..17d1d5dab 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
diff --git a/contrib/xml/doubleTypeInference.mli b/plugins/xml/doubleTypeInference.mli
index 2e14b5580..2e14b5580 100644
--- a/contrib/xml/doubleTypeInference.mli
+++ b/plugins/xml/doubleTypeInference.mli
diff --git a/contrib/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 407f86b36..407f86b36 100644
--- a/contrib/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
diff --git a/contrib/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml
index f7524671f..f7524671f 100644
--- a/contrib/xml/proof2aproof.ml
+++ b/plugins/xml/proof2aproof.ml
diff --git a/contrib/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index a501fb6a6..a501fb6a6 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
diff --git a/contrib/xml/theoryobject.dtd b/plugins/xml/theoryobject.dtd
index 953fe0092..953fe0092 100644
--- a/contrib/xml/theoryobject.dtd
+++ b/plugins/xml/theoryobject.dtd
diff --git a/contrib/xml/unshare.ml b/plugins/xml/unshare.ml
index f30f8230d..f30f8230d 100644
--- a/contrib/xml/unshare.ml
+++ b/plugins/xml/unshare.ml
diff --git a/contrib/xml/unshare.mli b/plugins/xml/unshare.mli
index 31ba90372..31ba90372 100644
--- a/contrib/xml/unshare.mli
+++ b/plugins/xml/unshare.mli
diff --git a/contrib/xml/xml.ml4 b/plugins/xml/xml.ml4
index e2d04cb76..e2d04cb76 100644
--- a/contrib/xml/xml.ml4
+++ b/plugins/xml/xml.ml4
diff --git a/contrib/xml/xml.mli b/plugins/xml/xml.mli
index 3775287a5..3775287a5 100644
--- a/contrib/xml/xml.mli
+++ b/plugins/xml/xml.mli
diff --git a/contrib/xml/xml_plugin.mllib b/plugins/xml/xml_plugin.mllib
index 3297ff068..3297ff068 100644
--- a/contrib/xml/xml_plugin.mllib
+++ b/plugins/xml/xml_plugin.mllib
diff --git a/contrib/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 1ae186614..1ae186614 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
diff --git a/contrib/xml/xmlcommand.mli b/plugins/xml/xmlcommand.mli
index 66ff9f0bb..66ff9f0bb 100644
--- a/contrib/xml/xmlcommand.mli
+++ b/plugins/xml/xmlcommand.mli
diff --git a/contrib/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4
index 41c107ad2..41c107ad2 100644
--- a/contrib/xml/xmlentries.ml4
+++ b/plugins/xml/xmlentries.ml4
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 811a0db2c..919aacbbe 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -320,7 +320,7 @@ let include_dirs (inc_i,inc_r) =
-I $(COQLIB)/proofs -I $(COQLIB)/tactics \\
-I $(COQLIB)/toplevel";
List.iter (fun c -> print " \\
- -I $(COQLIB)/contrib/"; print c) Coq_config.contrib_dirs; print "\n";
+ -I $(COQLIB)/plugins/"; print c) Coq_config.plugins_dirs; print "\n";
print "COQLIBS:="; print_list "\\\n " str_i'; print " "; print_list "\\\n " str_r; print "\n";
print "COQDOCLIBS:="; print_list "\\\n " str_r; print "\n\n"
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 07c8126f1..f6acd0b65 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -167,11 +167,11 @@ let coqdep () =
if not Coq_config.has_natdynlink then option_natdynlk := false;
if !Flags.boot then begin
add_rec_dir add_known "theories" ["Coq"];
- add_rec_dir add_known "contrib" ["Coq"]
+ add_rec_dir add_known "plugins" ["Coq"]
end else begin
let coqlib = Envars.coqlib () in
add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
- add_rec_dir add_coqlib_known (coqlib//"contrib") ["Coq"];
+ add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
add_dir add_coqlib_known (coqlib//"user-contrib") []
end;
List.iter (fun (f,d) -> add_mli_known f d) !mliAccu;
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 67113aa06..59fe701aa 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -12,8 +12,8 @@ open Coqdep_common
(** [coqdep_boot] is a stripped-down version of [coqdep], whose
behavior is the one of [coqdep -boot]. Its only dependencies
- are [Coqdep_lexer] and [Unix], and it should stay so.
- If it need someday some additional information, pass it via
+ are [Coqdep_lexer], [Coqdep_common] and [Unix], and it should stay so.
+ If it needs someday some additional information, pass it via
options (see for instance [option_natdynlk] below).
*)
@@ -29,7 +29,7 @@ let coqdep_boot () =
if Array.length Sys.argv < 2 then exit 1;
parse (List.tl (Array.to_list Sys.argv));
add_rec_dir add_known "theories" ["Coq"];
- add_rec_dir add_known "contrib" ["Coq"];
+ add_rec_dir add_known "plugins" ["Coq"];
List.iter (fun (f,d) -> add_mli_known f d) !mliAccu;
List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu;
List.iter (fun (f,_,d) -> add_ml_known f d) !mlAccu;
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 90a36620a..e736fc676 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -97,11 +97,11 @@ let theories_dirs_map = [
let init_load_path () =
let coqlib = Envars.coqlib () in
let user_contrib = coqlib/"user-contrib" in
- let dirs = "states" :: ["contrib"] in
+ let dirs = ["states";"plugins"] in
(* first user-contrib *)
if Sys.file_exists user_contrib then
Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
- (* then states, contrib and dev *)
+ (* then states, theories and dev *)
List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
(* developer specific directory to open *)
if Coq_config.local then coq_add_path (coqlib/"dev") "dev";