diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 33 |
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 = { |