From 9894cffae9662f0473ab3f8696e8ca498cc9cdec Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 21 Jun 2018 17:37:33 +0200
Subject: Remove quote plugin

As far as I know, this plugin is untested and barely maintained. I don't
think it has real use cases any more, so let's move it out from the repo
and see if somebody wants to take over and maintain it.

We also remove the documentation, which was telling our users to look at
ring to see an example of reification done using quote, when in fact it
wasn't using it anymore.
---
 Makefile.common | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index 09457ced7b..69dea1d284 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -95,7 +95,7 @@ CORESRCDIRS:=\
   tactics 	vernac		stm		toplevel
 
 PLUGINDIRS:=\
-  omega		romega 		micromega 	quote \
+  omega		romega 		micromega \
   setoid_ring 	extraction \
   cc 		funind 		firstorder 	derive \
   rtauto 	nsatz           syntax          btauto \
@@ -131,7 +131,6 @@ GRAMMARCMA:=grammar/grammar.cma
 OMEGACMO:=plugins/omega/omega_plugin.cmo
 ROMEGACMO:=plugins/romega/romega_plugin.cmo
 MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo
-QUOTECMO:=plugins/quote/quote_plugin.cmo
 RINGCMO:=plugins/setoid_ring/newring_plugin.cmo
 NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo
 EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo
@@ -152,7 +151,7 @@ SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
 SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
 
 PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
-        $(QUOTECMO) $(RINGCMO) \
+        $(RINGCMO) \
         $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
         $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \
-- 
cgit v1.2.3