aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--plugins/ssrsearch/g_search.mlg2
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg2
2 files changed, 4 insertions, 0 deletions
diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index 6d68cc13ab..f5cbf2005b 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -2,6 +2,8 @@
(* Main prefilter *)
+DECLARE PLUGIN "ssrsearch_plugin"
+
{
module CoqConstr = Constr
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 8979170026..3af39ec59a 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -8,6 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+DECLARE PLUGIN "ltac2_plugin"
+
{
open Pp