From 4476f64dc87fb86738fc4c9f939113b70843c035 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 18 Sep 2020 14:15:18 +0200
Subject: {new,setoid_}ring -> ring

I believe this renaming makes it easier for new contributors to discover
the code of `ring`.
---
 Makefile.common | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index 8f880e93fb..a482b9b963 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -103,7 +103,7 @@ CORESRCDIRS:=\
 
 PLUGINDIRS:=\
   omega		micromega \
-  setoid_ring 	extraction \
+  ring 	extraction \
   cc 		funind 		firstorder 	derive \
   rtauto 	nsatz           syntax          btauto \
   ssrmatching	ltac		ssr             ssrsearch
@@ -140,7 +140,7 @@ CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/l
 
 OMEGACMO:=plugins/omega/omega_plugin.cmo
 MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo
-RINGCMO:=plugins/setoid_ring/newring_plugin.cmo
+RINGCMO:=plugins/ring/ring_plugin.cmo
 NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo
 EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo
 FUNINDCMO:=plugins/funind/recdef_plugin.cmo
-- 
cgit v1.2.3