Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

1 files changed, 17 insertions, 16 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 7f42a747..c3181e4c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -253,24 +253,25 @@ let declare_sideff env fix_exn se =
                if Constant.equal c c' then Some (x,kn) else None) inds_consts)
            knl))
 
-let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
-  let cd = (* We deal with side effects of non-opaque constants *)
+let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
+  let cd = (* We deal with side effects *)
     match cd with
-    | Entries.DefinitionEntry ({
-      const_entry_opaque = false; const_entry_body = bo } as de)
-    | Entries.DefinitionEntry ({
-      const_entry_polymorphic = true; const_entry_body = bo } as de)
-      ->
-        let _, seff = Future.force bo in
-        if Declareops.side_effects_is_empty seff then cd
-        else begin
-          let seff = Declareops.uniquize_side_effects seff in
-          Declareops.iter_side_effects
-            (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff;
-          Entries.DefinitionEntry { de with
-            const_entry_body = Future.chain ~pure:true bo (fun (pt, _) ->
-              pt, Declareops.no_seff) }
+    | Entries.DefinitionEntry de ->
+        if export_seff ||
+           not de.const_entry_opaque ||
+           de.const_entry_polymorphic then
+          let bo = de.const_entry_body in
+          let _, seff = Future.force bo in
+          if Declareops.side_effects_is_empty seff then cd
+          else begin
+            let seff = Declareops.uniquize_side_effects seff in
+            Declareops.iter_side_effects
+              (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff;
+            Entries.DefinitionEntry { de with
+              const_entry_body = Future.chain ~pure:true bo (fun (pt, _) ->
+                pt, Declareops.no_seff) }
         end
+        else cd
     | _ -> cd
   in
   let cst = {