aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term_typing.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-03-12 20:16:43 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-03-23 16:33:26 +0100
commitee1546dc6686e888cc8da5f9442bcf788544dd0e (patch)
tree1084a85dfe1b5a72cd0aa3d0a162f02149dd2c43 /kernel/term_typing.mli
parentea8185d872f242f8ebf4274ebe550ed81107150a (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/term_typing.mli')
0 files changed, 0 insertions, 0 deletions