diff options
| author | Pierre-Marie Pédrot | 2019-04-24 16:03:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-10 12:53:09 +0200 |
| commit | a5a89e8b623cd5822f59b854a45efc8236ae0087 (patch) | |
| tree | 8950d13c0d8f75c14724191d58f100c78206a4d3 /kernel/nativecode.ml | |
| parent | 4785156d31eb513b6e7fcb8dbab1c219da83612b (diff) | |
Logic.convert_hyp now takes an environment as an argument.
This prevents having to call global functions, for no good reason.
We also seize the opportunity to name the check argument.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions