From 32fb1656e7d98b77af43fd72889e9da9fa391a82 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 10 Oct 2018 20:25:15 +0200
Subject: [quote] Remove spurious file after deletion of quote plugin.

For some reason PR #7894 left this spurious file; this is typical of a
bad resolution of a merge, and while the file is innocuous it should
go away.
---
 plugins/setoid_ring/plugin_base.dune | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/setoid_ring/plugin_base.dune')

diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/plugin_base.dune
index 101246e28f..d83857edad 100644
--- a/plugins/setoid_ring/plugin_base.dune
+++ b/plugins/setoid_ring/plugin_base.dune
@@ -2,4 +2,4 @@
  (name newring_plugin)
  (public_name coq.plugins.setoid_ring)
  (synopsis "Coq's setoid ring plugin")
- (libraries coq.plugins.quote))
+ (libraries coq.plugins.ltac))
-- 
cgit v1.2.3