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/term_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/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 082ed7ed0..5914c4a95 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -55,7 +55,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * unit constant_entry * side_effect_role + constant * constant_body * side_effect_role (* Given a constant entry containing side effects it exports them (either * by re-checking them or trusting them). Returns the constant bodies to @@ -65,9 +65,6 @@ val export_side_effects : structure_body -> env -> side_effects constant_entry -> exported_side_effect list * unit constant_entry -val constant_entry_of_side_effect : - constant_body -> seff_env -> unit constant_entry - val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body |