aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-09-17 16:16:39 +0000
committerGitHub2020-09-17 16:16:39 +0000
commit08791151b904e499cdca26cec4b8aa7c9b1eb4c0 (patch)
tree583b907530ea9c77bdec3d1bf11488f7ef5d00c1 /plugins
parent14f0e5059e7f49cabbcd1571d7f053db7d7d3f35 (diff)
parent29b8aae282f03fcd7d753d19129e5f74feacc820 (diff)
Merge PR #13007: [build] Don't link `num` anymore in Coq
Reviewed-by: Zimmi48 Reviewed-by: vbgl Ack-by: Zimmi48 Ack-by: vbgl
Diffstat (limited to 'plugins')
-rw-r--r--plugins/micromega/dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/dune b/plugins/micromega/dune
index 33ad3a0138..204125ab56 100644
--- a/plugins/micromega/dune
+++ b/plugins/micromega/dune
@@ -4,7 +4,7 @@
; be careful not to link the executable to the plugin!
(modules (:standard \ csdpcert g_zify zify))
(synopsis "Coq's micromega plugin")
- (libraries num coq.plugins.ltac))
+ (libraries coq.plugins.ltac))
(executable
(name csdpcert)