aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/dune
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax/dune')
-rw-r--r--plugins/syntax/dune7
1 files changed, 0 insertions, 7 deletions
diff --git a/plugins/syntax/dune b/plugins/syntax/dune
index b395695c8a..1b3d7598da 100644
--- a/plugins/syntax/dune
+++ b/plugins/syntax/dune
@@ -13,13 +13,6 @@
(libraries coq.vernac))
(library
- (name r_syntax_plugin)
- (public_name coq.plugins.r_syntax)
- (synopsis "Coq syntax plugin: reals")
- (modules r_syntax)
- (libraries coq.vernac))
-
-(library
(name int63_syntax_plugin)
(public_name coq.plugins.int63_syntax)
(synopsis "Coq syntax plugin: int63")