Merge PR #11539: [dune] [stdlib] Build the standard library natively with Dune.

Reviewed-by: Zimmi48

15 files changed, 30 insertions, 0 deletions

diff --git a/plugins/btauto/plugin_base.dune b/plugins/btauto/dune
index 6a024358c3..d2f5b65980 100644
--- a/plugins/btauto/plugin_base.dune
+++ b/plugins/btauto/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.btauto)
  (synopsis "Coq's btauto plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_btauto))
diff --git a/plugins/cc/plugin_base.dune b/plugins/cc/dune
index 2a92996d2a..f7fa3adb56 100644
--- a/plugins/cc/plugin_base.dune
+++ b/plugins/cc/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.cc)
  (synopsis "Coq's congruence closure plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_congruence))
diff --git a/plugins/derive/plugin_base.dune b/plugins/derive/dune
index ba9cd595ce..1931339471 100644
--- a/plugins/derive/plugin_base.dune
+++ b/plugins/derive/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.derive)
  (synopsis "Coq's derive plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_derive))
diff --git a/plugins/extraction/plugin_base.dune b/plugins/extraction/dune
index 037b0d5053..0c01dcd488 100644
--- a/plugins/extraction/plugin_base.dune
+++ b/plugins/extraction/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.extraction)
  (synopsis "Coq's extraction plugin")
  (libraries num coq.plugins.ltac))
+
+(coq.pp (modules g_extraction))
diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/dune
index d88daa23fc..1b05452d8f 100644
--- a/plugins/firstorder/plugin_base.dune
+++ b/plugins/firstorder/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.firstorder)
  (synopsis "Coq's first order logic solver plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_ground))
diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/dune
index 6ccf15df29..e594ffbd02 100644
--- a/plugins/funind/plugin_base.dune
+++ b/plugins/funind/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.funind)
  (synopsis "Coq's functional induction plugin")
  (libraries coq.plugins.extraction))
+
+(coq.pp (modules g_indfun))
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/dune
index 5611f5ba16..6558ecbfe8 100644
--- a/plugins/ltac/plugin_base.dune
+++ b/plugins/ltac/dune
@@ -11,3 +11,5 @@
  (synopsis "Coq's tauto tactic")
  (modules tauto)
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules extratactics g_tactic  g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs))
diff --git a/plugins/micromega/plugin_base.dune b/plugins/micromega/dune
index 4153d06161..33ad3a0138 100644
--- a/plugins/micromega/plugin_base.dune
+++ b/plugins/micromega/dune
@@ -20,3 +20,5 @@
  (modules g_zify zify)
  (synopsis "Coq's zify plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_micromega g_zify))
diff --git a/plugins/nsatz/plugin_base.dune b/plugins/nsatz/dune
index 9da5b39972..b921c9c408 100644
--- a/plugins/nsatz/plugin_base.dune
+++ b/plugins/nsatz/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.nsatz)
  (synopsis "Coq's nsatz solver plugin")
  (libraries num coq.plugins.ltac))
+
+(coq.pp (modules g_nsatz))
diff --git a/plugins/omega/plugin_base.dune b/plugins/omega/dune
index f512501c78..0db71ed6fb 100644
--- a/plugins/omega/plugin_base.dune
+++ b/plugins/omega/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.omega)
  (synopsis "Coq's omega plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_omega))
diff --git a/plugins/rtauto/plugin_base.dune b/plugins/rtauto/dune
index 233845ae0f..43efa0eca5 100644
--- a/plugins/rtauto/plugin_base.dune
+++ b/plugins/rtauto/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.rtauto)
  (synopsis "Coq's rtauto plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_rtauto))
diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/dune
index d83857edad..60522cd3f5 100644
--- a/plugins/setoid_ring/plugin_base.dune
+++ b/plugins/setoid_ring/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.setoid_ring)
  (synopsis "Coq's setoid ring plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_newring))
diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/dune
index a13524bb52..a117d09a16 100644
--- a/plugins/ssr/plugin_base.dune
+++ b/plugins/ssr/dune
@@ -5,3 +5,5 @@
  (modules_without_implementation ssrast)
  (flags :standard -open Gramlib)
  (libraries coq.plugins.ssrmatching))
+
+(coq.pp (modules ssrvernac ssrparser))
diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/dune
index 06f67c3774..629d723816 100644
--- a/plugins/ssrmatching/plugin_base.dune
+++ b/plugins/ssrmatching/dune
@@ -3,3 +3,5 @@
  (public_name coq.plugins.ssrmatching)
  (synopsis "Coq ssrmatching plugin")
  (libraries coq.plugins.ltac))
+
+(coq.pp (modules g_ssrmatching))
diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/dune
index 512752135d..b395695c8a 100644
--- a/plugins/syntax/plugin_base.dune
+++ b/plugins/syntax/dune
@@ -32,3 +32,5 @@
  (synopsis "Coq syntax plugin: float")
  (modules float_syntax)
  (libraries coq.vernac))
+
+(coq.pp (modules g_numeral g_string))