diff options
| author | Pierre-Marie Pédrot | 2019-06-08 16:50:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-11 16:59:08 +0200 |
| commit | 929ecfe0cd8cd3edec41416491e286e4c105ffa6 (patch) | |
| tree | 74acaf09aae9dec751c430e4c8bb0127b06cc363 /interp/declare.mli | |
| parent | e753855167e5629775b604128c6efc9d58ee626c (diff) | |
Move the side-effect role out of Entries into Evd.
Diffstat (limited to 'interp/declare.mli')
| -rw-r--r-- | interp/declare.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/declare.mli b/interp/declare.mli index ed76f0a284..e2485d7cf0 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -56,7 +56,7 @@ val declare_constant : ?internal:internal_flag -> ?local:import_status -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t val declare_private_constant : - role:side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects + ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> |