diff options
| author | Maxime Dénès | 2018-06-21 17:37:33 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-12 17:04:42 +0200 |
| commit | 9894cffae9662f0473ab3f8696e8ca498cc9cdec (patch) | |
| tree | cf4f5c2366e4a74faa24c33317b2ac802ffc195c /Makefile.common | |
| parent | e3e1f56c38f345bccf984dd6d6d86fa06e423b96 (diff) | |
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.
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 5 |
1 files changed, 2 insertions, 3 deletions
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) \ |