diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssrsearch/g_search.mlg | 2 |
1 files changed, 2 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 |