diff options
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index fcd95576c..89b5fc40e 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -30,6 +30,7 @@ val inline_entry_side_effects : yet type checked proof. *) val uniq_seff : side_effects -> side_effects +val equal_eff : side_effect -> side_effect -> bool val translate_constant : structure_body -> env -> constant -> side_effects constant_entry -> |