From 4a53151f846476f2fbe038a4ecb8e84256a26ba9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 14 Feb 2015 18:35:04 +0100 Subject: Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior Of course such proofs cannot be processed asynchronously --- library/declare.ml | 33 +++++++++++++++++---------------- 1 file changed, 17 insertions(+), 16 deletions(-) (limited to 'library/declare.ml') diff --git a/library/declare.ml b/library/declare.ml index 7f42a747e..c3181e4c7 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 = { -- cgit v1.2.3