aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/dune (renamed from plugins/btauto/plugin_base.dune)2
-rw-r--r--plugins/cc/dune (renamed from plugins/cc/plugin_base.dune)2
-rw-r--r--plugins/derive/dune (renamed from plugins/derive/plugin_base.dune)2
-rw-r--r--plugins/extraction/dune (renamed from plugins/extraction/plugin_base.dune)2
-rw-r--r--plugins/firstorder/dune (renamed from plugins/firstorder/plugin_base.dune)2
-rw-r--r--plugins/funind/dune (renamed from plugins/funind/plugin_base.dune)2
-rw-r--r--plugins/ltac/dune (renamed from plugins/ltac/plugin_base.dune)2
-rw-r--r--plugins/micromega/dune (renamed from plugins/micromega/plugin_base.dune)2
-rw-r--r--plugins/nsatz/dune (renamed from plugins/nsatz/plugin_base.dune)2
-rw-r--r--plugins/omega/dune (renamed from plugins/omega/plugin_base.dune)2
-rw-r--r--plugins/rtauto/dune (renamed from plugins/rtauto/plugin_base.dune)2
-rw-r--r--plugins/setoid_ring/dune (renamed from plugins/setoid_ring/plugin_base.dune)2
-rw-r--r--plugins/ssr/dune (renamed from plugins/ssr/plugin_base.dune)2
-rw-r--r--plugins/ssrmatching/dune (renamed from plugins/ssrmatching/plugin_base.dune)2
-rw-r--r--plugins/syntax/dune (renamed from plugins/syntax/plugin_base.dune)2
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))