aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorPierre Letouzey2017-06-16 17:40:04 +0200
committerPierre Letouzey2018-03-06 18:24:28 +0100
commita768e75f761ae444c05162ec1d064795d413ba25 (patch)
treed8d501dda29040c3e750b1077785833675ab3a43 /kernel/nativecode.mli
parentdf9d3a36e71d6d224286811fdc529ad5a955deb7 (diff)
romega: get rid of EConstr.Unsafe
We replace constr by EConstr.t everywhere, and propagate some extra sigma args
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions