aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorBruno Barras2013-12-17 19:34:48 +0100
committerBruno Barras2013-12-17 19:34:48 +0100
commit370fe53d6c1c56919feae24192b390b1c2dc491e (patch)
treef64875b1531b0aeae55c88689aa184d486e407e9 /kernel/nativecode.ml
parent30b58d43e48569afb50a35d3915ec7d453a61f5d (diff)
test guard condition against feature incompatible with prop-ext
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions