diff options
| author | letouzey | 2012-07-05 22:51:11 +0000 |
|---|---|---|
| committer | letouzey | 2012-07-05 22:51:11 +0000 |
| commit | 2ed6aeb03fc0e25a47223189d8444cbb6b749f2d (patch) | |
| tree | 653de6038f3247ef8e18610ad07f1b83c6f253b5 /Makefile.common | |
| parent | afe903e7889625986edab5506e3bb2cb90f7f483 (diff) | |
Legacy Ring and Legacy Field migrated to contribs
One slight point to check someday : fourier used to
launch a tactic called Ring.polynom in some cases.
It it crucial ? If so, how to replace with the setoid_ring
equivalent ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/Makefile.common b/Makefile.common index 5ce5442f8b..1ede038364 100644 --- a/Makefile.common +++ b/Makefile.common @@ -74,9 +74,9 @@ SRCDIRS:=\ pretyping interp toplevel/utils toplevel parsing \ printing grammar intf ide/utils ide \ $(addprefix plugins/, \ - omega romega micromega quote ring \ + omega romega micromega quote \ setoid_ring xml extraction fourier \ - cc funind firstorder field \ + cc funind firstorder \ rtauto nsatz syntax decl_mode btauto) # Order is relevent here because kernel and checker contain files @@ -166,10 +166,8 @@ 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 +RINGCMA:=plugins/setoid_ring/newring_plugin.cma NSATZCMA:=plugins/nsatz/nsatz_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 @@ -188,7 +186,7 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ - $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(FIELDCMA) \ + $(QUOTECMA) $(RINGCMA) \ $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \ $(CCCMA) $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \ $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) @@ -300,9 +298,7 @@ OMEGAVO:=$(call cat_vo_itarget, plugins/omega) ROMEGAVO:=$(call cat_vo_itarget, plugins/romega) MICROMEGAVO:=$(call cat_vo_itarget, plugins/micromega) QUOTEVO:=$(call cat_vo_itarget, plugins/quote) -RINGVO:=$(call cat_vo_itarget, plugins/ring) -FIELDVO:=$(call cat_vo_itarget, plugins/field) -NEWRINGVO:=$(call cat_vo_itarget, plugins/setoid_ring) +RINGVO:=$(call cat_vo_itarget, plugins/setoid_ring) NSATZVO:=$(call cat_vo_itarget, plugins/nsatz) FOURIERVO:=$(call cat_vo_itarget, plugins/fourier) FUNINDVO:=$(call cat_vo_itarget, plugins/funind) @@ -312,9 +308,9 @@ EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction) XMLVO:= CCVO:= -PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ +PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) \ $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \ - $(RTAUTOVO) $(BTAUTOVO) $(NEWRINGVO) $(QUOTEVO) \ + $(RTAUTOVO) $(BTAUTOVO) $(RINGVO) $(QUOTEVO) \ $(NSATZVO) $(EXTRACTIONVO) ALLVO:= $(THEORIESVO) $(PLUGINSVO) |