From 2ed6aeb03fc0e25a47223189d8444cbb6b749f2d Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 5 Jul 2012 22:51:11 +0000
Subject: 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
---
 Makefile.common | 18 +++++++-----------
 1 file changed, 7 insertions(+), 11 deletions(-)

(limited to 'Makefile.common')

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)
-- 
cgit v1.2.3