Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior

Of course such proofs cannot be processed asynchronously

2 files changed, 18 insertions, 17 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 7f42a747ed..c3181e4c75 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 = {
diff --git a/library/declare.mli b/library/declare.mli
index 03b66271a2..d8a00db0cf 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -53,7 +53,7 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types ->
   constr -> definition_entry
 
 val declare_constant :
- ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> constant
+ ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->