aboutsummaryrefslogtreecommitdiff
path: root/kernel/typeops.mli
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-05-04 11:18:34 +0200
committerEmilio Jesus Gallego Arias2020-05-18 19:08:19 +0200
commitc8b54d74bc7cf29cc04d0a3cedbf4a106f6e744c (patch)
tree18a0bf70119a51f0bf6ec6262ddfefd9790b8005 /kernel/typeops.mli
parent809291d5ef7371bfe8841b95126c0332da55578f (diff)
[declare] Merge `DeclareObl` into `Declare`
This is needed as a first step to refactor and unify the obligation save path and state; in particular `Equations` is a heavy user of Hooks to modify obligations state, thus in order to make the hook aware of this we need to place the obligation state before the hook. As a good side-effect, `inline_private_constants` and `Hook.call` are not exported from `Declare` anymore.
Diffstat (limited to 'kernel/typeops.mli')
0 files changed, 0 insertions, 0 deletions