aboutsummaryrefslogtreecommitdiff
path: root/kernel/genOpcodeFiles.ml
diff options
context:
space:
mode:
authorPierre Roux2020-06-18 20:12:36 +0200
committerPierre Roux2020-06-18 20:22:52 +0200
commitd958feb5f30255d3b9ca84bf5be89c299ddb8a5f (patch)
tree4c200b9fb278ccb2f0d990a856bb211682d30adc /kernel/genOpcodeFiles.ml
parent33e763a441022623621536766ac38c3021dcb65c (diff)
Fix #12228 negative integers not accepted in ltac integer_list
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions