aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/dune
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax/dune')
-rw-r--r--plugins/syntax/dune17
1 files changed, 5 insertions, 12 deletions
diff --git a/plugins/syntax/dune b/plugins/syntax/dune
index 1b3d7598da..f930fc265a 100644
--- a/plugins/syntax/dune
+++ b/plugins/syntax/dune
@@ -1,15 +1,8 @@
(library
- (name numeral_notation_plugin)
- (public_name coq.plugins.numeral_notation)
- (synopsis "Coq numeral notation plugin")
- (modules g_numeral numeral)
- (libraries coq.vernac))
-
-(library
- (name string_notation_plugin)
- (public_name coq.plugins.string_notation)
- (synopsis "Coq string notation plugin")
- (modules g_string string_notation)
+ (name number_string_notation_plugin)
+ (public_name coq.plugins.number_string_notation)
+ (synopsis "Coq number and string notation plugin")
+ (modules g_number_string string_notation number)
(libraries coq.vernac))
(library
@@ -26,4 +19,4 @@
(modules float_syntax)
(libraries coq.vernac))
-(coq.pp (modules g_numeral g_string))
+(coq.pp (modules g_number_string))