diff options
| author | Emilio Jesus Gallego Arias | 2020-09-14 18:26:21 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-09-15 15:57:43 +0200 |
| commit | acb24a1540c33f075a83f9788614e5c2f3335b0a (patch) | |
| tree | 1985cc10a9685e9dfb60b6d96a050e9d588d7070 /kernel/vmbytecodes.ml | |
| parent | 7bf884b7c525092db74ac2effcf1091bd3c3d46c (diff) | |
[micromega] Use `minus_one` built-in zarith constant.
Diffstat (limited to 'kernel/vmbytecodes.ml')
0 files changed, 0 insertions, 0 deletions