diff options
| author | Emilio Jesus Gallego Arias | 2020-05-29 12:20:03 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-29 12:20:03 +0200 |
| commit | d75b889948fbfd5600d505ab823a0e6da2195af6 (patch) | |
| tree | 85b5c543e8b5ab1c0cb87227d605725d8ebec36b | |
| parent | 7c21e568501b16cc99ecd79afd9e26a912b89ca5 (diff) | |
| parent | 19c8ac834c4f43b1fd0c49aad286a4e5bebf0ce5 (diff) | |
Merge PR #12421: Fixes for compilation without native dynlink
Reviewed-by: ejgallego
Reviewed-by: ppedrot
| -rw-r--r-- | plugins/ssrsearch/g_search.mlg | 2 | ||||
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 2 | ||||
| -rw-r--r-- | vernac/mltop.ml | 3 |
3 files changed, 7 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 diff --git a/vernac/mltop.ml b/vernac/mltop.ml index d276a1ac35..c33b3d29f8 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -309,6 +309,9 @@ type ml_module_object = { } let add_module_digest m = + if not has_dynlink then + m, NoDigest + else try let file = file_of_name m in let path, file = System.where_in_path ~warn:false !coq_mlpath_copy file in |