diff options
| author | Hugo Herbelin | 2020-05-28 16:47:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-28 17:02:55 +0200 |
| commit | 19c8ac834c4f43b1fd0c49aad286a4e5bebf0ce5 (patch) | |
| tree | 27d970d8818c394e7a78b13891727856c9a0a159 | |
| parent | 5e0907df8a8711dcdbe92dc3a34225d32b300d0b (diff) | |
Adding missing DECLARE PLUGIN so that compilation with -natdynlink no works.
| -rw-r--r-- | plugins/ssrsearch/g_search.mlg | 2 | ||||
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 2 |
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 |