diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-16 00:05:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:12:10 +0200 |
| commit | ce830b204ad52f8b3655d2cb4672662120d83101 (patch) | |
| tree | 988e160ecf888787c6d005b08db0cdfd62935460 /kernel/safe_typing.mli | |
| parent | 3fcf0930874d7200f2503ac7084b1d6669d59540 (diff) | |
Further simplication: do not recreate entries for side-effects.
This is actually useless, the code does not depend on the value of the
entry for side-effects.
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 715226107..148fdca67 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -103,7 +103,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * unit Entries.constant_entry * private_constant_role + constant * private_constant_role val export_private_constants : in_section:bool -> private_constants Entries.constant_entry -> |