aboutsummaryrefslogtreecommitdiff
path: root/kernel/genOpcodeFiles.ml
diff options
context:
space:
mode:
authorPierre Roux2020-09-03 13:12:00 +0200
committerPierre Roux2020-11-04 20:53:47 +0100
commit11a8997dd8fa83537607272692a3baf10dab342a (patch)
tree2b88f003ab19f264d94f29806c28b48258800d28 /kernel/genOpcodeFiles.ml
parentdfcb15141a19db4f1cc61c14d1cdad0275009356 (diff)
[numeral notation] Adding the via ... using ... option
This enables numeral notations for non inductive types by pre/postprocessing them to a given proxy inductive type. For instance, this should enable the use of numeral notations for R.
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions