aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/plugin_base.dune
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
-rw-r--r--plugins/syntax/plugin_base.dune22
1 files changed, 7 insertions, 15 deletions
diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune
index bfdd480fe9..1ab16c700d 100644
--- a/plugins/syntax/plugin_base.dune
+++ b/plugins/syntax/plugin_base.dune
@@ -6,6 +6,13 @@
(libraries coq.plugins.ltac))
(library
+ (name string_notation_plugin)
+ (public_name coq.plugins.string_notation)
+ (synopsis "Coq string notation plugin")
+ (modules g_string string_notation)
+ (libraries coq.vernac))
+
+(library
(name r_syntax_plugin)
(public_name coq.plugins.r_syntax)
(synopsis "Coq syntax plugin: reals")
@@ -13,23 +20,8 @@
(libraries coq.vernac))
(library
- (name ascii_syntax_plugin)
- (public_name coq.plugins.ascii_syntax)
- (synopsis "Coq syntax plugin: ASCII")
- (modules ascii_syntax)
- (libraries coq.vernac))
-
-(library
- (name string_syntax_plugin)
- (public_name coq.plugins.string_syntax)
- (synopsis "Coq syntax plugin: strings")
- (modules string_syntax)
- (libraries coq.plugins.ascii_syntax))
-
-(library
(name int31_syntax_plugin)
(public_name coq.plugins.int31_syntax)
(synopsis "Coq syntax plugin: int31")
(modules int31_syntax)
(libraries coq.vernac))
-