diff options
| author | Emilio Jesus Gallego Arias | 2018-10-10 20:25:15 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-10 21:07:59 +0200 |
| commit | 32fb1656e7d98b77af43fd72889e9da9fa391a82 (patch) | |
| tree | 97e74dc4b85097be50bc311d1befeaa0f3e6a170 /plugins/setoid_ring | |
| parent | 040ad198e38776bb9f398329243b2fe41434f2d5 (diff) | |
[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.
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/plugin_base.dune | 2 |
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)) |