diff options
| author | Pierre-Marie Pédrot | 2017-02-01 10:52:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-01 10:54:53 +0100 |
| commit | c17c3faee20251cd5c7168246e9ffcd12d557f85 (patch) | |
| tree | 02635866b73d7595fad009cc17535a6bbf06c2fc /kernel/term_typing.mli | |
| parent | f86bfa39cddfb9c6411ed8624cee9a2b5c8d53bd (diff) | |
| parent | 568b38e1d599f8bac5adf140f5a114f2871bc436 (diff) | |
Merge branch 'v8.6'
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 fcd95576c0..89b5fc40e3 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 -> |