aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring/plugin_base.dune
diff options
context:
space:
mode:
authorThéo Zimmermann2018-10-11 14:35:50 +0200
committerThéo Zimmermann2018-10-11 14:35:50 +0200
commit4a6ddf4fdc4790fc407dc98bcfb80fd816cab304 (patch)
treea28536dae55101f5643d7eb6ce1f64c71660afac /plugins/setoid_ring/plugin_base.dune
parentea62cca89773e8101b7a81d15adbf15081eb5e0f (diff)
parent32fb1656e7d98b77af43fd72889e9da9fa391a82 (diff)
Merge PR #8699: [quote] Remove spurious file after deletion of quote plugin.
Diffstat (limited to 'plugins/setoid_ring/plugin_base.dune')
-rw-r--r--plugins/setoid_ring/plugin_base.dune2
1 files changed, 1 insertions, 1 deletions
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))