From 5e0907df8a8711dcdbe92dc3a34225d32b300d0b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 28 May 2020 16:46:07 +0200
Subject: Fixing compilation with -natdynlink no.

This complements #11407 about storing digests of modules.
---
 vernac/mltop.ml | 3 +++
 1 file changed, 3 insertions(+)

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
-- 
cgit v1.2.3


From 19c8ac834c4f43b1fd0c49aad286a4e5bebf0ce5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 28 May 2020 16:47:30 +0200
Subject: Adding missing DECLARE PLUGIN so that compilation with -natdynlink no
 works.

---
 plugins/ssrsearch/g_search.mlg | 2 ++
 user-contrib/Ltac2/g_ltac2.mlg | 2 ++
 2 files changed, 4 insertions(+)

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
-- 
cgit v1.2.3