diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-12 20:16:43 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-23 16:33:26 +0100 |
commit | ee1546dc6686e888cc8da5f9442bcf788544dd0e (patch) | |
tree | 1084a85dfe1b5a72cd0aa3d0a162f02149dd2c43 /kernel/opaqueproof.mli | |
parent | ea8185d872f242f8ebf4274ebe550ed81107150a (diff) |
Using a dedicated datastructure for side effect ordering.
We were doing fishy things in the Term_typing file, where side-effects were
not considered in the right uniquization order because of the uniq_seff_rev
function. It probably did not matter after a9b76df because effects were
(mostly) uniquize upfront, but this is not clear because of the use of the
transparente API in the module.
Now everything has to go through the opaque API, so that a proper dependence
order is ensured.
Diffstat (limited to 'kernel/opaqueproof.mli')
0 files changed, 0 insertions, 0 deletions